VDM specification language

From Free net encyclopedia

Current revision

Template:Cleanup-date

VDM Specification Language (VDM-SL) is a model-oriented specification language, upon which the Vienna Development Method for computer software is based. An ISO Standard for the language was released in 1996 (ISO, 1996).

The origins of VDM-SL lie in the IBM Laboratory in Vienna where the first version of the language, then called Meta-IV (Bjørner et al. 1978), was used to describe the PL/I programming language. Other programming languages 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 (Jones 1980, 1990). 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" (Bjørner et al. 1982) has tended to stress a constructive approach with explicit operational specification used to a greater extent. Danish work led to the first European validated Ada compiler.

Language

Symbols

ext

rd

wr

pre

post

card

::

mk-Name

inv-Name

[...]

dom

rng

hd

tl

len

elems

Syntax

VDM-SL makes use of [[propositional logic|propositional calculus] and predicate logic.

In BNF notation, the available operators for propositional logic are:

<math>proposition\ ::=\ letter</math>

<math>| \quad \lnot\ proposition</math>

<math>| \quad proposition \land proposition</math>

<math>| \quad proposition \lor proposition</math>

<math>| \quad proposition \Rightarrow proposition</math>

<math>| \quad proposition \Leftrightarrow proposition</math>

<math>| \quad (proposition)</math>

Precidence is in the order:

1. Brackets
2. <math>\lnot</math> (not)
3. <math>\land</math> (and)
4. <math>\lor</math> (or)
5. <math>\Rightarrow</math> (implies)
6. <math>\Leftrightarrow</math> (equivanence)

The syntax for predicate logic is:
<math>sentence\ ::=\ simple\underline{\ }term</math>

<math>| \quad predicate </math>

<math>| \quad \lnot\ sentence</math>

<math>| \quad sentence \land sentence</math>

<math>| \quad sentence \lor sentence</math>

<math>| \quad sentence \Rightarrow sentence</math>

<math>| \quad sentence \Leftrightarrow sentence</math>

<math>| \quad \forall variable\underline{\ }name \bullet sentence</math>

<math>| \quad \exists variable\underline{\ }name \bullet sentence</math>

<math>| \quad (sentence)</math>

<math>simple\underline{\ }term ::= upper\underline{\ }case\underline{\ }letter;</math>
<math>predicate ::= predicate\underline{\ }name(term\underline{\ }list);</math>
<math>term ::= proper\underline{\ }name;</math>

<math>| \quad arbitrary\underline{\ }name;</math>

<math>| \quad variable\underline{\ }name;</math>

<math>term\underline{\ }list ::= term;</math>

<math>| \quad term, term\underline{\ }list;</math>

<math>predicate\underline{\ }name ::= string;</math>
<math>proper\underline{\ }name ::= string;</math>
<math>arbitrary\underline{\ }name ::= lower\underline{\ }case\underline{\ }letter;</math>
<math>variable\underline{\ }name ::= lower\underline{\ }case\underline{\ }letter;</math>

Functions

VDM functions are defined as:

Signature

Pre-conditions

Post-conditions

The whole point of VDM is to prove that functions are correct; this is called a proof obligation.

Suppose that we have an implicit specification:

<math>f(p:T_p)r:T_r</math>

pre pre-f(p)

post post-f(p, r)

When we define an explicit function:

<math>f:T_p \rightarrow T_r</math>

we say it satisfies the specification iff it obeys the proof obligation:

<math>\forall p \in T_p \bullet pre\mbox{-}f(p) \Rightarrow f(p) \in T_r \land post\mbox{-}f(p, f(p))</math>

So, "f is a correct implementation" should be interpreted as "f satisfies the specification".

States and operations

In VDM-SL, functions are not allowed to have side-effects (such as changing the state of a global variable). This is a useful ability in many programming languages, so a similar concept exists; instead of functions, operators are used to change states (AKA globals).

For example, if we have a state consisting of a single variable <math>someStateRegister : \mathbb{N}</math>, we could define this in VDM-SL as:

<math>\mbox{state}\ Register\mbox{ of}</math>

<math>\qquad someStateRegister : \mathbb{N}</math>

<math>\mbox{end}\ </math>

An operation to load a value into this variable might be specified as:

<math>LOAD(i : \mathbb{N})</math>

<math>\mbox{ext wr}\ someStateRegister : \mathbb{N}</math>

<math>\mbox{post}\ someStateRegister = i</math>

The exterior clause (ext) specifies which parts of the state can be accessed by the operation; rd meaning read access and wr being read/write access.

Sometimes it is important to refer to the value of a state before it was modified; for example, an operation to add a value to the variable may be specified as:

<math>ADD(i : \mathbb{N})</math>

<math>\mbox{ext wr}\ someStateRegister : \mathbb{N}</math>

<math>\mbox{post}\ someStateRegister = \begin{matrix}\leftharpoonup \\ someStateRegister \end{matrix} + i</math>

Where the <math>\leftharpoonup</math> symbol tells one to use the initial state of (in this case) someStateRegister.

Composite Types

The general form of a composite type definition is:

<math>Name::</math>

<math>s_1 : T_1</math>

<math>s_2 : T_2</math>

<math>\vdots</math>

<math>s_n : T_n</math>

(Where "Name" is the name of the type, not the string literal "Name"). A type has an associated constructor:

<math>mk\mbox{-}Name : T_1 \times T_2 \times \cdots T_n \to Name</math>

and selector functions:

<math>Name::</math>

<math>s_1 : Name -> T_1</math>

<math>s_2 : Name -> T_2</math>

<math>\vdots</math>

<math>s_n : Name -> T_n</math>

Example

<math>Date::</math>

<math>day : \{1, \cdots, 366\}</math>

<math>year : \{1901, \cdots, 2099\}</math>

<math>mk-Date : \{1, \cdots, 366\} \times \{1901,\cdots,2099\} \to Date</math>

<math>day : Date \to \{1, \cdots, 366\}</math>

<math>year : Date \to \{1901,\cdots,2099\}</math>

This might be called with <math>mk-Date(45, 2003)</math>.

Note that this would also need some extra checking, as day 366 is only valid on leap years. For example, the function <math>valid\mbox{-}Date(dt) \to \mathbb{B}</math> may be implemented as:

<math>valid\mbox{-}Date(dt) \underline{\Delta} is\mbox{-}leapyear(year(dt)) \or day(dt) \le 365</math>

<math>is\mbox{-}leapyear(i) \underline{\Delta} i\mbox{ mod }4 = 0</math>

(Note: this definition of leap year works only because of the limits on the range of the year variable, demonstrating that it is still entirely possible to introduce errors into VDM systems).

Optional Fields

Optional fields are allowed in composite types, denoted by [...], and an omitted field is denoted by nil.

For example, the composite type "Record" may be defined with:

<math>Record::</math>

<math>day : \{1,\cdots,366\}</math>

<math>year : \{1901,\cdots,2099\}</math>

<math>valid : [ERROR]</math>

which may be called with:

<math>mk-Record(366, 2004, \mbox{nil}) \in Record</math>

<math>k-Record(366, 2003, ERROR) \in Record</math>

Optional fields allow composite types to be recursive.

Maps

A map is similar to a function defined on a finite set, except that the argument/result pairs are given explicitly, e.g. <math>\{a_1 \mapsto r_1, a_2 \mapsto r_2, \cdots, a_n \mapsto r_n\}</math>. See map (mathematics) for more information.

Maps in VDM-SL are denoted by the form <math>X -m-> Y</math>, e.g. <math>\mathbb{Z} -m-> \mathbb{N}</math>.

For example, <math>\{a,b\} -m-> \{1,2\}</math> is the set of maps:

<math>\{ \{\mapsto\},</math>

<math>\{a \mapsto 1\}, \{a \mapsto 2\},</math>

<math>\{b \mapsto 1\}, \{b \mapsto 2\},</math>

<math>\{a \mapsto 1, b \mapsto 1\}, \{a \mapsto 1, b \mapsto 2\},</math>

<math>\{a \mapsto 2, b \mapsto 1\}, \{a \mapsto 2, b \mapsto 2\} \}</math>

If m is a map, dom m is the domain of m, rng m is the range of m and m(x) means m applied to x, e.g., if <math>m = \{a \mapsto 1, b \mapsto 3, c \mapsto 5, d \mapsto 7\}</math> then <math>\mbox{dom }m = \{a, b, c, d\}</math>, <math>\mbox{rng }m = \{1, 3, 5, 7\}</math>, m(a) = 1, m(b) = 3, etc.

Map Overriding

Overriding is a map operation, denoted by <math>m_1 \dagger m_2</math>, which causes the elements of m₂ to override the elements of m₁. For example, given:

<math>m_1 = \{a \mapsto 1, b \mapsto 2\}</math>

<math>m_2 = \{a \mapsto 2, c \mapsto 2\}</math>

then <math>m_1 \dagger m_2 = \{a \mapsto 2, b \mapsto 2, c \mapsto 2\}</math>.

Bank system example

Customers are modelled by customer numbers (CustNum), accounts are modelled by account numbers (AccNum).

<math>Bank::</math>

<math>accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData</math>

<math>overdraftMap : CustNum \begin{matrix} m \ o \end{matrix} Overdraft</math>

where

<math>inv\mbox{-}Bank(mk\mbox{-}Bank(accountMap, overdraftMap))\underline{\Delta}</math>

<math>\quad \forall mk\mbox{-}AccData(CustNum, balance) \in\mbox{ rng } AccNum \ \bullet</math>

<math>\quad CustNum \in \mbox{ dom } overdraftMap \land balance \ge -overdraftMap(CustNum)</math>

<math>AccData::</math>

<math>owner : CustNum</math>

<math>balance : Balance</math>

<math>Overdraft = \mathbb{N}</math>

<math>Balance = \mathbb{Z}</math>

With operations: NEWC allocates a new customer number:

<math>NEWC(od : Overdraft)r : CustNum</math>

<math>\mbox{ext wr }odm : CustNum \begin{matrix} m \ o \end{matrix} Overdraft</math>

<math>\mbox{post }r \notin \mbox{ dom } \begin{matrix}\leftharpoonup \\ overdraftMap \end{matrix} \land overdraftMap = \begin{matrix}\leftharpoonup \\ overdraftMap \end{matrix} \dagger \{r \mapsto od\}</math>

NEWAC allocates a new account number and sets the balance to zero:

<math>NEWAC(cu : CustNum)r : AccNum</math>

<math>\mbox{ext rd } overdraftMap : CustNum \begin{matrix} m \ o \end{matrix} Overdraft</math>

<math>\quad \mbox{wr } accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData</math>

<math>\mbox{pre } cu e \mbox{ dom } overdraftMap</math>

<math>\mbox{post } r \notin \mbox{ dom } \begin{matrix}\leftharpoonup \\ accountMap \end{matrix} \land accountMap = \begin{matrix}\leftharpoonup \\ accountMap \end{matrix} \dagger \{r \mapsto mk\mbox{-}AccData)cu, 0)\}</math>

ACINF returns all the balances of all the accounts of a customer, as a map of account number to balance:

<math>ACINF(cu : CustNum)r : AccNum \begin{matrix} m \ o \end{matrix} Balance</math>

<math>\mbox{ext rd } accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData</math>

<math>\mbox{post } r = \{AccNum \mapsto balance(accountMap(AccNum)) |</math>

<math>\quad \quad AccNum e \mbox{ dom } accountMap \land owner(accountMap(AccNum)) = cu\}</math>

Sequences

It is possible to have sequences of elements of some type X. The type of such a sequence is denoted by X^*, while the sequences themselves are denoted by, e.g., [a, b, c] where <math>a, b, c \in X</math>. The empty sequence is [].

The order and repetition of items in a sequence is significant, so <math>[a, b] \ne [b, a]</math>, and <math>[a] \ne [a, a]</math>, which means that X^* is infinite even when X itself is finite (e.g. <math>[a], [a, a], [a, a, a], \cdots</math>).

Sequence operations

VDL-SL has the following sequence operations:

Provided 1 ≤ i ≤ len s, s(i) is the i^th element of s.

Examples

The max function

<math>max(i : \mathbb{Z}, j : \mathbb{Z})r : \mathbb{Z}</math>

<math>pre\ true</math>

<math>post (r = i \lor r = j) \land i \le r \land j \le r</math>

Natural number multiplication

<math>multp(i : \mathbb{N}, j : \mathbb{N})r : \mathbb{N}</math>

<math>pre\ true</math>

<math>post\ r = i*j</math>

Applying the proof obligation <math>\forall p \in T_p \bullet pre-f(p) \Rightarrow f(p) \in T_r \land post-f(p, f(p))</math> to an explicit definition of multip:

<math>multp(i,j) \underline{\triangle}</math>

<math>\mbox{if}\ i=0</math>

<math>\mbox{then}\ 0</math>

<math>\mbox{else if}\ is\mbox{-}even(i)</math>

<math>\mbox{then}\ 2*multp(i/2,\ j)</math>

<math>\mbox{else}\ j + multp(i-1,\ j)</math>

Then the proof obligation becomes:

<math>\forall i, j \in \mathbb{N} \bullet multp(i, j) \Rightarrow f(p) \in \mathbb{N} \land multp(i, j) = i*j</math>

This can be shown correct by the following steps:

1. Proving that the recursion ends (this in turn requires proving that the numbers become smaller at each step)
2. Mathematical induction

Mathematical operators

The following notation describe partially the operators +, mod, and /; and also the function is divisible by?:

Queue abstract data type

<math>\mbox{types}</math>

<math>Qelt = \mbox{To Be Defined}</math>

<math>Queue = Quelt^*</math>

<math>\mbox{state }TheQueue\mbox{ of}</math>

<math>q : Queue</math>

<math>\mbox{end}</math>

<math>\mbox{operations}</math>

<math>ENQUEUE (e : Qelt)</math>

<math>\mbox{ext wr }q : Queue</math>

<math>\mbox{post }q = \begin{matrix}\leftharpoonup \\ q \end{matrix} (curvy arrow thing) [e];</math>

<math>DEQUEUE() e : Qelt</math>

<math>\mbox{ext wr }q : Queue</math>

<math>\mbox{pre }q \ne []</math>

<math>\mbox{post }\begin{matrix}\leftharpoonup \\ q \end{matrix} = [e] (curvy arrow thing) q;</math>

<math>IS\mbox{-}EMPTY() r : \mathbb{B}</math>

<math>\mbox{ext rd }q : Queue</math>

<math>\mbox{post }r \Leftrightarrow (\mbox{len }q = 0)</math>

See also

• Formal methods
• Formal specification
• Predicate logic
• Propositional calculus
• Vienna Development Method
• Z specification language, the main alternative to VDM-SL (compare)

External links

• VDM standard

References

• D. Bjorner and C. B. Jones (eds.), The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science, Vol. 61, Springer-Verlag 1978. ISBN 0387087664
• D. Bjørner and C. B. Jones, Formal Specification and Software Development Prentice Hall International, 1982. ISBN 0138807337
• J. Dawes, The VDM-SL Reference Guide, Pitman 1991. ISBN 0273031511
• J. S. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques for Software Development, Cambridge University Press, 1998, ISBN 0521623480
• J. S. Fitzgerald, P. G. Larsen, P. Mukherjee, N. Plat and M. Verhoef. Validated Designs for Object-oriented Systems, Springer Verlag, 2005. ISBN 1852338814
• International Organization for Standardisation, Information technology – Programming languages, their environments and system software interfaces – Vienna Development Method - Specification Language – Part 1: Base language International Standard ISO/IEC 13817-1, December 1996.
• C. B. Jones, Systematic Software Development Using VDM, Prentice Hall International, 1990. ISBN 0138807256
• C. B. Jones, Software Development: A Rigorous Approach, Prentice Hall International, 1980. ISBN 0138218846
• C. B. Jones and R. Shaw (eds.), Case Studies in Systematic Software Development, Prentice Hall International, 1990. ISBN 0138807337