Vienna Development Method

From Wikipedia, the free encyclopedia

Vienna Development Method (VDM) is a program development method based on formal specification using the VDM specification language (VDM-SL), with tool support. There is an object-oriented extension, VDM++.

1 The development cycle
- 1.1 Data Reification
  - 1.1.1 Example data reification
2 External links
3 References
- 3.1 Books

[edit] The development cycle

Use of VDM starts with a very abstract specification and, develops this into an implementation. Each step involves Data Reification, then Operation Decomposition.

Data reification develops the abstract data types into more concrete data structures, while operation decomposition develops the (abstract) implicit specifications of operations and functions into algorithms that can be directly implemented in a computer language of choice.

Specification		Implementation
Abstract data type	––– Data reification →	Data structure
Operations	––– Operation decomposition →	Algorithms

[edit] Data Reification

Data reification involves finding a more concrete representation of the abstract data types used in a specification. There may be several steps before an implementation is reached. Each step involves:

Given an abstract data representation "ABS_REP", find a new representation "NEW_REP".
Find a "retrieve function" that relates ABS_REP to NEW_REP, i.e. retr : NEW_REP → ABS_REP
Prove that NEW_REP is sufficient for representing ABS_REP, i.e. prove that $\forall a \in ABS\_REP \bullet \exists r \in NEW\_REP \bullet a = retr(r)$
Rewrite the operations and functions in terms of NEW_REP
Prove that the new operations and functions preserve any data-type invariants of the new representation
Prove that the new operations and functions model those found in the original specification. This involves two rules:
- Domain rule: $\forall r \in NEW\_REP \bullet \mbox{pre-}OPA(retr(r)) \Rightarrow \mbox{pre-}OPR(r)$
- Modelling rule: $\forall \begin{matrix}\leftharpoonup \\ r \end{matrix}, r \in NEW\_REP \bullet \mbox{pre-}OPA(retr(\begin{matrix}\leftharpoonup \\ r \end{matrix})) \land \mbox{post-}OPR(\begin{matrix}\leftharpoonup \\ r \end{matrix}, r) \Rightarrow \mbox{post-}OPA(retr(\begin{matrix}\leftharpoonup \\ r \end{matrix}), retr(r))$

[edit] Example data reification

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:

INIT() — initialises the system, assumes that the factory is empty
ENTER(p : Person) — records that a worker is entering the factory; the workers' details are read from the ID card)
EXIT(p : Person) — records that a worker is exiting the factory
IS-PRESENT(p : Person) r : $\mathbb{B}$ — checks to see if a specified worker is in the factory or not

Formally, this would be:
types

Person = To be defined

Workers = Person-set

state AWCCS of

pres : Workers

end
operations

INIT()

ext wr pres : Workers

post pres = {};

ENTER(p : Person)

ext wr pres : Workers

pre p pres

post pres = {p};

EXIT(p : Person)

ext wr pres : Workers

pre p pres

post pres = - {p};

IS-PRESENT(p : Person) r :

ext rd pres : Workers

post r p pres

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. These sequences must not allow repetition, as we do not want the same worker to appear twice, so we must add an invariant to the new data type. In this case, ordering is not important, so [a, b] is the same as [b, a].

The Vienna Development Method is valuable for model-based systems. It is not appropriate if the system is time-based. For such cases, the Concurrent Calculus System (CCS) is more useful.