Usage description

Although the implementation resulting from this project is not yet finished, with some additional manual steps it can already be used. Furthermore, it can easily be setup for further development. This page describes how to setup the system and how to perform some basic actions using the code.

Setting up

Setting up the system itself is relatively easy. It consists of two components: the translator and the prover.

Translator setup

When using VDMTools, the sources can be opened directly using the following steps:

1. Extract the contents of the zip file
2. Open the VDMTools program
3. Open the VdmHolTranslator project from the root of the zip file

The directory structure of the translator is as follows:

• lib Containing any libraries required to run the project
  • astspec Containing the OML AST
  • io.vpp Containing IO functions, of which mainly the echo function is used
  • util.vpp Containing auxiliary functions, of which mainly the integer to string conversion is used
• src Containing any source files specific for this project
  • framework Containing any auxiliary files to the translation (HOL AST classes, proof obligation class, MLExpression class, etc.)
  • translator Containing the actual translator code and an error class
• VdmHolTranslator.prj The project file

Any of the files that can be found in the lib directory are libraries and were not written in this project. They can be replaced by new versions if these are available (and assuming these are backward compatible).

Proof system setup

For the proof system, HOL4 is required (any earlier version will not work). Installation instructions and downloads can be found here: http://hol.sourceforge.net. The system can be installed automatically on Windows and from sources on (at least) Windows, Unix-like systems and Mac OS-X. Note that the installation from sources may take a while as it will proof all theorems in the libraries during installation. Once HOL4 is installed and functioning properly, the setup for the proof is complete.

Usage

As mentioned above, the system is not yet complete. Although eventually it should be possible to run the entire system pressing just one button, currently, a lot of steps have to be performed manually. Below a description of a possible usage of the system is explained.

Translator usage

The translator system itself can be accessed in various ways. One of the main approaches is to translate a VDM AST (or OML AST) to a HOL AST. Both AST's are represented by classes in the code. The OML AST (which also supports most VDM++ models) is defined by the OvertureParser, the HOL AST by this translator. The translation can be performed by calling a single function on a new translator object:

new VdmHolTranslator().translateDocument(document)

The parameter document should be an OML AST like the one that can be obtained directly from the OvertureParser. The result will be a HOL document. This HOL document can be written to concrete code by calling its print function on it:

someHolDocument.print()

This will result in a string, which one could print to the screen using the echo function in the IO toolbox (if desired). The contents of the string can be used as input to HOL. Note however that the translation is not complete, in some cases, the translation will not be accepted by the HOL engine. Components of the translation that have not been completed yet can be found in AutomaticProofOpenIssues.

When using the translator for proof, one most likely would also like to translate the proof obligations. Since these proof obligations require some further processing, these steps have also been automated by the DocumentProver class. This class can be constructed using a HOL document and a set of proof obligations. These two will be merged during which several issues are resolved that mainly have to do with dependencise between the two. By calling the getProofCounter function on the DocumentProver, an expression will be constructed that when inserted into HOL, will try to prove all obligations and count the number of successes. The code to generate this is:

someDocumentProver.getProofCounter().print()

Proof system usage

Once the document is translated, doing the proof attempts is relatively straightforward:

1. Start the HOL engine (for example by executing hol in the bin directory of the HOL installation)
2. Copy all content from the tactics file (AutomaticProofDownloads) into the HOL engine. This will load all additional libraries, prove additional theorems and declare the tactics.
3. Copy the translated document into the HOL engine (with or without proof obligations, depending on whether one would like to try the proof attempts or not).

Once the proof attempts are finished, interpretation of the results may be more complex. Figuring out whether a proof is succesful or not is usually doable, but analyzing where a failed proof attempt went wrong is much more complex. When using the document prover, each line starting with:

val success = success + boolToInteger...

is a proof attempt. This attempt will increase the value of the success variable (which counts the number of successes) by one every time a proof attempt is succesful. The success variable and its content are printed at every proof atempt by HOL automatically, from which one can deduce the result of the proof attempt.

-- SanderVermolen - 26 Feb 2008