Proof automation architecture

This page will give a high-level overview of the steps involved in automated proof. If not familiar with automated proof, some of the topics that are addressed in this page may require additional explanation to be understood fully. A full explanation of these and a more complete version of this text can be found in thesisSanderVermolen.pdf.

The main part of the proof automation consists of three steps:

• Preparation in which the input VDM model is converted to a format suitable for processing and the proof obligations that need to be proved are generated;
• Translation in which the output of the previous step is converted to a format providing the basis for the final HOL model and
• Proof in which the actual HOL model is generated and an attempt to prove the obligations is made.

The following sections will focus on each of them individually.

Preparation

Although a concrete VDM model is very suitable for human processing, in automated processes a more explicitly structured and usually somewhat more redundant representation is preferred. A tree structure is easier to process than the linear text in the model and components of the model that have been assigned their specific function are easier to process than components of which the function must be deduced from the context. The OvertureParser will be used to convert any given OML model to a more structured and more redundant representation. We will refer to the result of this conversion as the VDM Abstract Syntax Tree (VDM AST) or when an entire VDM model was used as input, the abstract VDM model.

The second task in preparation is the generation of the proof obligations of the model. They are usually extracted from the AST generated in the previous task and will also usually be provided as small VDM AST's. Also for this task, software exists to perform it, unfortunately it has not yet been developed within Overture. Therefore, the VDMTools set, specifically its integrity checker, will be used.

Translation

Neither the VDM AST nor the concrete syntax VDM model can be used directly as input to the HOL engine. HOL uses its own language to express models and to control the engine. A translation from VDM to HOL is thus required. Using the abstract VDM model and the proof obligations from the preparation phase, the first task of this step involves this translation. The translator that is defined and implemented in this project, uses the abstract VDM model as input and produces an abstract HOL model as output. Since also the proof obligations are available as VDM abstract syntax trees from the previous step, the same translation can be used to convert these.

The entire translation has been specified as an executable VDM model itself. This model can be interpreted to execute the translation. When finished, most likely Java code will be generated from the translator model, which is then compiled and interpreted to perform the translation. But this Java code generation is already possible if desired.

Once translated, we enter the 'HOL domain'. From now on, all processing will be in HOL terms (either concrete or abstract). The second task of the translation will be a merge of the proof obligations and the model. Apart from just joining the two code bases, this merge also consists of type rewritings of the proof obligations using the document's definitions.

Proof

This is the final and seemingly most important part of the process is the proof. Using the abstract HOL model and its proof obligations resulting from the previous step, there are two tasks left to before actually using the HOL engine:

• HOL code generation This involves serializing the abstract HOL syntax tree to a concrete HOL model, such that it can be used as input to a HOL session.
• HOL tactics selection A good tactic is crucial for being able to prove the obligation and being able to do it in a reasonable amount of time.

Once we have our concrete HOL model, and selected tactics, we can start the proof attempts themselves. This starts by loading all required libraries into HOL, followed by loading the model and selected tactics. Next, the attempts to prove each of the individual proof obligations will finish the work started in the previous steps.

-- SanderVermolen - 18 Jan 2008