Vienna Development Method
The Vienna Development Method is one of the longest-established formal methods for the development of computer-based systems. Originating in work done at the IBM Laboratory Vienna in the 1970s, it has grown to include a group of techniques and tools based on a formal specification language—the VDM Specification Language. It has an extended form, VDM++, which supports the modeling of object-oriented and concurrent systems. Support for VDM includes commercial and academic tools for analyzing models, including support for testing and proving properties of models and generating program code from validated VDM models. 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.
Philosophy
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. It also has an executable subset, so that models may be analyzed by testing and can be executed through graphical user interfaces, so that models can be evaluated by experts who are not necessarily familiar with the modeling language itself.History
The origins of VDM-SL lie in the IBM Laboratory in Vienna where the first version of the language was called the Vienna Definition Language. The VDL was essentially used for giving operational semantics descriptions in contrast to the VDM – Meta-IV which provided denotational semantics
«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 overall approach adopted has been termed the "Vienna Development Method"... The meta-language actually adopted is used to define major portions of PL/1 in BEKIČ 74.»
There is no connection between Meta-IV, and Schorre's META II language, or its successor Tree Meta; these were compiler-compiler systems rather than being suitable for formal problem descriptions.
So Meta-IV was "used to define major portions of" the PL/I programming language. Other programming languages retrospectively described, or partially described, using Meta-IV and VDM-SL include the BASIC programming language, FORTRAN, the APL programming language, ALGOL 60, the Ada programming language and the Pascal programming language. Meta-IV evolved into several variants, generally described as the Danish, English and Irish Schools.
The "English School" derived from work by Cliff Jones on the aspects of VDM not specifically related to language definition and compiler design. It stresses modelling persistent state through the use of data types constructed from a rich collection of base types. 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" has tended to stress a constructive approach with explicit operational specification used to a greater extent. Work in the Danish school led to the first European validated Ada compiler.
An ISO Standard for the language was released in 1996.
VDM features
The VDM-SL and VDM++ syntax and semantics are described at length in the VDMTools language manuals and in the available texts. The ISO Standard contains a formal definition of the language's semantics. In the remainder of this article, the ISO-defined interchange syntax is used. Some texts prefer a more concise mathematical syntax.A VDM-SL model is a system description given in terms of the functionality performed on data. It consists of a series of definitions of data types and functions or operations performed upon them.
Basic types: numeric, character, token and quote types
VDM-SL includes basic types modelling numbers and characters as follows:Data types are defined to represent the main data of the modelled system. Each type definition introduces a new type name and gives a representation in terms of the basic types or in terms of types already introduced. For example, a type modelling user identifiers for a log-in management system might be defined as follows:
types
UserId = nat
For manipulating values belonging to data types, operators are defined on the values. Thus, natural number addition, subtraction etc. are provided, as are Boolean operators such as equality and inequality. The language does not fix a maximum or minimum representable number or a precision for real numbers. Such constraints are defined where they are required in each model by means of data type invariants—Boolean expressions denoting conditions that must be respected by all elements of the defined type. For example, a requirement that user identifiers must be no greater than 9999 would be expressed as follows :
UserId = nat
inv uid uid <= 9999
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.
The other basic types include char for characters. In some cases, the representation of a type is not relevant to the model's purpose and would only add complexity. In such cases, the members of the type may be represented as structureless tokens. Values of token types can only be compared for equality – no other operators are defined on them. Where specific named values are required, these are introduced as quote types. Each quote type consists of one named value of the same name as the type itself. Values of quote types may only be compared for equality.
For example, in modelling a traffic signal controller, it may be convenient to define values to represent the colours of the traffic signal as quote types:
Type constructors: union, product and composite types
The basic types alone are of limited value. New, more structured data types are built using type constructors. | Union of types T1,...,Tn |
T1*T2*...*Tn | Cartesian product of types T1,...,Tn |
T :: f1:T1... fn:Tn | Composite type |
The most basic type constructor forms the union of two predefined types. The type
B. In the traffic signal controller example, the type modelling the colour of a traffic signal could be defined as follows:SignalColour =
Enumerated types in VDM-SL are defined as shown above as unions on quote types.
Cartesian product types may also be defined in VDM-SL. The type
A1 and the second from the type A2 and so on. The composite or record type is a Cartesian product with labels for the fields. The typeT :: f1:A1
f2:A2
...
fn:An
is the Cartesian product with fields labelled
f1,…,fn. An element of type T can be composed from its constituent parts by a constructor, written mk_T. Conversely, given an element of type T, the field names can be used to select the named component. For example, the typeDate :: day:nat1
month:nat1
year:nat
inv mk_Date d<=31 and m<=12
models a simple date type. The value
mk_Date corresponds to 1 April 2001. Given a date d, the expression d.month is a natural number representing the month. Restrictions on days per month and leap years could be incorporated into the invariant if desired. Combining these:mk_Date.month = 4
Collections
Collection types model groups of values. Sets are finite unordered collections in which duplication between values is suppressed. Sequences are finite ordered collections in which duplication may occur and mappings represent finite correspondences between two sets of values.Sets
The set type constructor constructs the type composed of all finite sets of values drawn from the typeT. For example, the type definitionUGroup = set of UserId
defines a type
UGroup composed of all finite sets of UserId values. Various operators are defined on sets for constructing their union, intersections, determining proper and non-strict subset relationships etc. | Set enumeration: the set of elements a, b and c |
| Set comprehension: the set of x from type T such that P |
| The set of integers in the range i to j |
e in set s | e is an element of set s |
e not in set s | e is not an element of set s |
s1 union s2 | Union of sets s1 and s2 |
s1 inter s2 | Intersection of sets s1 and s2 |
s1 \ s2 | Set difference of sets s1 and s2 |
dunion s | Distributed union of set of sets s |
s1 psubset s2 | s1 is a subset of s2 |
s1 subset s2 | s1 is a subset of s2 |
card s | The cardinality of set s |