Open issues

Although the system may work for the case studies, it is not yet completed for main stream usage. This page shows a list of the known issues that prevent this main stream usage. The issues are categorized by their context: the translator, the proof support, or anything else which I have named 'framework'.

VDM to HOL Translator

• Several unsupported language constructs (e.g. union patterns and disjunction patterns). Most of these are basic and can easily be translated, some may be harder to add. Each unsupported language construct will produce an unknown ... error when it is used anyway. There is no complete list of what is not implemented. A complete list of what is implemented can directly be derived from the VDMToHolTranslator file in the sources. If you would like constructs to be added, which are currently not supported, feel free to contact me.
• Map application Although the map application can be used in your VDM files, it is not translated as a map application in HOL, but as a function application. So what should become (FAPPLY someMap someValue) in HOL (the regular HOL map application), will become (someMap someValue). This will produce a type error when reading the generated model into HOL. To solve this, one currently has to substitute the map applications manually in the HOL model. This cannot be solved yet, due to the fact that type information is not available at VDM to HOL translation time.
• Record type name tagging The record should be tagged with a the record type name, but is not. As a result, the comparison of two records that have the same sets of field names and furthermore, for each field the same value, but are of a different type, will in VDM not be equal, but in HOL will be equal (of course this is unlikely and obviously solved if there are no two record types that have exactly the same set of field names and of which, above all, two instances are compared).
• Invariant propagation The reintroduction of invariants as described in section 3.5.2 of the extensive project description (downloads section) is not implemented for function definitions or type definitions (meaning: recursive usage of invariants in type definitions). The invariant reintroduction is implemented for quantifiers, comprehensions and other type binds. The fact that it is not implemented for functions will not produce problems in execution and should not have any influence on the result when used in combination with the regular VDM proof obligation generators, since these have a redundancy in invariant checking that solves exactly this issue. It is not solved for recursive usage of invariants in type definitions, but this is an issue of the proof obligation generator, not so much of this tool. In short: this issue should not have any influence on the usage or result of this tool when it is used to proof the proof obligations. When used for other purposes, consider to add the invariants manually to the VDM model, to whatever you would like to proof, or to the HOL model, each of these will work. More information can be found in the description mentioned above.

Proof support

• There are no known issues about the proof support, other than it is not user friendly yet if you do not know HOL (there is no GUI) and interpretation of the results will have to be done manually.

Framework

• There is no integration of the different steps yet. All will have to be done manually, which works, but requires some background knowledge.
• There is not enough documentation on usage of the tool yet. This web site is the best documentation regarding that aspect. The thesis that can be found in the downloads section documents the ideas, principles and techniques behind the tool.

-- SanderVermolen - 17 Jan 2008