Download Formal Methods for System Development

2.2 Selected specification languages
2.2
Selected specification languages
The Vienna Development Method and the Z notation are two dominant formal specification methods. They are both rooted in mathematical notation
and are used to specify systems at an abstracted level. They differ mainly
in that Z is only a specification language, while VDM is a complete method,
describing a possible work process from specification to implementation.
2.2.1
Vienna Development Method
The Vienna Development Method (VDM) contains both a specification language, and a complete method for development. Its specification language
VDM-SL is based on predicate logic and mathematical constructs such as
sets.
The steps involved in VDM can be explained as follows [10]:
1. Formally specify the system.
2. Prove that the specification is consistent.
3. Refine and decompose the specification, and prove that the new realisation satisfies the previous specification.
4. Repeat above step until the realisation is appropriately concrete.
5. Revise the above steps.
Of note here is the last step. It says that part of the development method
is to inspect the steps themselves. Different projects benefit from slightly
different steps, and different time allotted. E.g. some may only need one
step for refinement, others may need much time for the initial specification.
Usage example: Abstract queue
The specification language has a limit where a refinement becomes too complex and explicit. At some point the refined specification must become the
basis for implementation. This is the penultimate step in VDM, to stop
when the specification becomes appropriately concrete and implementation
is fairly straight forward.
On to the specification language itself, we have an example of a abstract
queue in Figure 2.1, gathered from [27]. This example shows some of the
main features in VDM-SL, such as types, state and operations. It is given
in the standardised ASCII notation.
The example has a state, TheQueue, which internally is given by the
variable q, which is a sequence of tokens. Sequences have an inherent ordering, unlike sets. There are three operations defined, which are like functions,
in that they specify valid operations. Each operation may include a pre- and
a post-condition. They can be used to implicitly describe what the operation
does.
5