VDMCore

From Wiki.overturetool.org

VDM Core

At the semantics workshop in London September 2010 it was suggested to come up with a core language where it is possible to define a simple semantics and enable the most valuable semantic analysis of VDM core models including formal verification. The intend is then that it shall be possible to define transformations from more user friendly VDM languages such as VDM-SL, VDM++ and VDM-RT (and possibly more future dialects). In this way a clean semantics can be obtained for the core and additional complexity desired can be moved to the transformations from the user-friendly languages to the VDM core. Ideally the Overture tool support shall carry out the similar kind of AST transformations exploiting the common core language where semantic analysis can be performed. Naturally in such a setting it will be advantagous if error messages can be reported back to the user relative to the model he is working on in the more user-friendly VDM language so this is a more long term target. Thus in parallel with the efforts in defining the VDM Core and its semantics and proof rules the existing Overture tool development will continue to be developed based on the existing technology.

The VDM core constructs are inspired by the paper Erik Ernst presented at the Overture semantics workshop. Basically it contains:

• Each class always have exactly one constructor that initialise all its instance variables (also for all its superclasses) and this happen atomically and any invariants ove instance variables must hold at completion of the constructor. The constructor can only assign to the instance variables using functional expressions (on the right hand side of the assignment operator). This means that general operation calls inside constructors are NOT allowed. A special kind of functions (currently called instance functions) can be used in the expressions.
• Instance variables cannot be initialised as a part of their declaration.
• Overloaded definitions are not allowed.
• No access modifiers are used in VDM Core (so in principle everything is public)
• When we have instance variables that only gets adjusted by the constructor we will term them "instance values" since they will be constant per instance of a class.
• When we have operations that operate only on instance values we will call them instance functions since they will have the functional transparency property inside each instance.
• A special GLOBAL class is used for all definitions that are globally available. Thus this is the place one can define data to be used for test purposes as well as static definitions (placed in ordinary classes in the more user friendly VDM++).

This work is initiated by moving some of the existing VDM model examples from the Overture SourceForge repository from VDM++ to become models written in the VDM Core language. So far this have been done for two examples from the VDM++ book:

• The Alarm example (relative simple example without inheritance)
• The Enigma example (a rather complex example with plenty of inheritance)

In order to be able to still use the existing version of Overture access modifiers are still included here but they are only there to enable the tools still to work. These are now checked into the Overture SourceForge repository in a new documentation/examples/VDMCode directory. Anybody else interested in this are encoraged to take more examples and change them in the same way into the new VDMCore repository. In order to optimise peoples time I recommend that whenever you start a new project please list it here below (with your name against it) and when it has been completed and checked in move it up to the list above.