There is a history of industrial usage of VDM and its tools and a growing body of research in the formalism has led to notable contributions to the engineering of critical systems, compilers, concurrent systems and in logic for computer science.
Computing systems may be modeled in VDM-SL at a higher level of abstraction than is achievable using programming languages, allowing the analysis of designs and identification of key features, including defects, at an early stage of system development.
Models that have been validated can be transformed into detailed system designs through a refinement process.
The language has a formal semantics, enabling proof of the properties of models to a high level of assurance.
[3] The VDL was essentially used for giving operational semantics descriptions in contrast to the VDM – Meta-IV which provided denotational semantics[4] «Towards the end of 1972 the Vienna group again turned their attention to the problem of systematically developing a compiler from a language definition.
The meta-language actually adopted ("Meta-IV") is used to define major portions of PL/1 (as given in ECMA 74 – interestingly a "formal standards document written as an abstract interpreter") in BEKIČ 74.»[5] There is no connection between Meta-IV,[6] and Schorre's META II language, or its successor Tree Meta; these were compiler-compiler systems rather than being suitable for formal problem descriptions.
Meta-IV evolved into several variants, generally described as the Danish, English and Irish Schools.
Functionality is typically described through operations which may have side-effects on the state and which are mostly specified implicitly using a precondition and postcondition.
The "Danish School" (Bjørner et al. 1982) has tended to stress a constructive approach with explicit operational specification used to a greater extent.
The VDM-SL and VDM++ syntax and semantics are described at length in the VDMTools language manuals and in the available texts.
For example, a requirement that user identifiers must be no greater than 9999 would be expressed as follows (where <= is the "less than or equal to" Boolean operator on natural numbers): Since invariants can be arbitrarily complex logical expressions, and membership of a defined type is limited to only those values satisfying the invariant, type correctness in VDM-SL is not automatically decidable in all situations.
Various operators are defined on sets for constructing their union, intersections, determining proper and non-strict subset relationships etc.
In VDM-SL there is a conventional modular extension whereas VDM++ has a traditional object-oriented structuring mechanism with classes and inheritance.
In the ISO standard for VDM-SL there is an informative annex that contains different structuring principles.
These all follow traditional information hiding principles with modules and they can be explained as: In VDM++ structuring are done using classes and multiple inheritance.
The precondition records the assumptions under which the function guarantees to return a result satisfying the postcondition.
If a function is called on inputs that do not satisfy its precondition, the outcome is undefined (indeed, termination is not even guaranteed).
The correctness of an explicit function definition with respect to an implicit specification may be defined as follows.
This is a useful ability in many programming languages, so a similar concept exists; instead of functions, operations are used to change state variables (also known as globals).
The function returns the largest element from a set of positive integers: The postcondition characterizes the result rather than defining an algorithm for obtaining it.
Applying the proof obligation forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p)) to an explicit definition of multp: Then the proof obligation becomes: This can be shown correct by: This is a classical example illustrating the use of implicit operation specification in a state-based model of a well-known data structure.
As a very simple example of a VDM-SL model, consider a system for maintaining details of customer bank account.
In order to show that the new representation is accurate, a retrieve function is defined that relates NEW_REP to ABS_REP, i.e. retr : NEW_REP -> ABS_REP.
In order to prove that the new operations and functions model those found in the original specification, it is necessary to discharge two proof obligations: In a business security system, workers are given ID cards; these are fed into card readers on entry to and exit from the factory.
Operations required: Formally, this would be: As most programming languages have a concept comparable to a set (often in the form of an array), the first step from the specification is to represent the data in terms of a sequence.