VDM specification language

From Wikipedia, the free encyclopedia

This article or section may require cleanup to meet Wikipedia's quality standards.
Please help improve this article or replace this tag with a more specific message. This article has been tagged since March 2006. (help, talk)

It has been suggested that this article or section be merged with Vienna_Development_Method. (Discuss)

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. Portuguese work led to the first European validated Ada compiler.

[edit] Language

[edit] Symbols

Basic Symbols
$\underline{\triangle}$	Is defined as
$\mathbb{B}$	(The set of) Booleans
$\mathbb{N}$	(the set of) natural numbers (including zero)
$\mathbb{N}_1$	(The set of) natural numbers (excluding zero)
$\mathbb{Z}$	(The set of) integers
$\mathbb{Q}$	(The set of) rational numbers
$\mathbb{R}$	(The set of) real numbers
:	Of type
ext	External clause
rd	Read access
wr	Write access
pre	Pre-condition
post	Post-condition
$\leftharpoonup$	The original value of

Sets
X-set	The type of sets of elements of X
${a, b, c}$	The set of elements a, b and c
${x \| P (x)}$	The set of x such that P(x)
${i,..., j}$	The set of integers in the range i to j
$\in$	Is an element of
$\notin$	Is not an element of
$\cup$	Union
$\cap$	Intersection
—	Set difference
$\bigcup$	Distributed union of
$\subset$	Is a (strict) subset of
$\subseteq$	Is a (weak) subset of
card	The cardinality of

Composite Types
::	Composite type of
mk-Name	make Name
inv-Name	invariant of Name
[...]	optional

Maps
$X \begin{matrix} m \\ \to \end{matrix} Y$	Y the type of maps from X to Y
$\{a \mapsto r, b \mapsto s\}$	a maps to r, b maps to s
$\{x \mapsto f(x) \| P(x)\}$	x maps to f(x) such that P(x)
dom	The domain of
rng	The range of
m(x)	m applied to x
$\dagger$	Overrides

Sequences
$X *$	The type of sequences of elements of X
[a, b, c]	The sequence of elements a, b and c
hd	The head of
tl	The tail of
len	The length of
elems	The elements of
$s (i)$	The i^th element of s
(curvy arrow thing)	concatenated with

[edit] Syntax

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

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

$proposition\ ::=\ letter$

$| \quad \lnot\ proposition$

$| \quad proposition \land proposition$

$| \quad proposition \lor proposition$

$| \quad proposition \Rightarrow proposition$

$| \quad proposition \Leftrightarrow proposition$

$| \quad (proposition)$

Precidence is in the order:

Brackets
$\lnot$ (not)
$\land$ (and)
$\lor$ (or)
$\Rightarrow$ (implies)
$\Leftrightarrow$ (equivanence)

The syntax for predicate logic is:
$sentence\ ::=\ simple\underline{\ }term$

$| \quad predicate$

$| \quad \lnot\ sentence$

$| \quad sentence \land sentence$

$| \quad sentence \lor sentence$

$| \quad sentence \Rightarrow sentence$

$| \quad sentence \Leftrightarrow sentence$

$| \quad \forall variable\underline{\ }name \bullet sentence$

$| \quad \exists variable\underline{\ }name \bullet sentence$

$| \quad (sentence)$

$simple\underline{\ }term ::= upper\underline{\ }case\underline{\ }letter;$
$predicate ::= predicate\underline{\ }name(term\underline{\ }list);$
$term ::= proper\underline{\ }name;$

$| \quad arbitrary\underline{\ }name;$

$| \quad variable\underline{\ }name;$

$term\underline{\ }list ::= term;$

$| \quad term, term\underline{\ }list;$

$predicate\underline{\ }name ::= string;$
$proper\underline{\ }name ::= string;$
$arbitrary\underline{\ }name ::= lower\underline{\ }case\underline{\ }letter;$
$variable\underline{\ }name ::= lower\underline{\ }case\underline{\ }letter;$

[edit] 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:

f (p : T p) r : T r

pre pre-f(p)

post post-f(p, r)

When we define an explicit function:

$f:T_p \rightarrow T_r$

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

$\forall p \in T_p \bullet pre\mbox{-}f(p) \Rightarrow f(p) \in T_r \land post\mbox{-}f(p, f(p))$

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

[edit] 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 $someStateRegister : \mathbb{N}$ , we could define this in VDM-SL as:

$\mbox{state}\ Register\mbox{ of}$

$\qquad someStateRegister : \mathbb{N}$

$\mbox{end}\$

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

$LOAD(i : \mathbb{N})$

$\mbox{ext wr}\ someStateRegister : \mathbb{N}$

$\mbox{post}\ someStateRegister = i$

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:

$ADD(i : \mathbb{N})$

$\mbox{ext wr}\ someStateRegister : \mathbb{N}$

$\mbox{post}\ someStateRegister = \begin{matrix}\leftharpoonup \\ someStateRegister \end{matrix} + i$

Where the $\leftharpoonup$ symbol tells one to use the initial state of (in this case) someStateRegister.

[edit] Composite Types

The general form of a composite type definition is:

N a m e ::

s 1 : T 1

s 2 : T 2

$\vdots$

s n : T n

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

$mk\mbox{-}Name : T_1 \times T_2 \times \cdots T_n \to Name$

and selector functions:

N a m e ::

s 1 : N a m e - > T 1

s 2 : N a m e - > T 2

$\vdots$

s n : N a m e - > T n

[edit] Example

D a t e ::

$day : \{1, \cdots, 366\}$

$year : \{1901, \cdots, 2099\}$

$mk-Date : \{1, \cdots, 366\} \times \{1901,\cdots,2099\} \to Date$

$day : Date \to \{1, \cdots, 366\}$

$year : Date \to \{1901,\cdots,2099\}$

This might be called with $m k - D a t e (45,2003)$ .

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

$valid\mbox{-}Date(dt) \underline{\Delta} is\mbox{-}leapyear(year(dt)) \or day(dt) \le 365$

$is\mbox{-}leapyear(i) \underline{\Delta} i\mbox{ mod }4 = 0$

(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).

[edit] 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:

R e c o r d ::

$day : \{1,\cdots,366\}$

$year : \{1901,\cdots,2099\}$

v a l i d :[E R R O R]

which may be called with:

$mk-Record(366, 2004, \mbox{nil}) \in Record$

$k-Record(366, 2003, ERROR) \in Record$

Optional fields allow composite types to be recursive.

[edit] Maps

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

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

For example, ${a, b} - m - > {1,2}$ is the set of maps:

$\{ \{\mapsto\},$

$\{a \mapsto 1\}, \{a \mapsto 2\},$

$\{b \mapsto 1\}, \{b \mapsto 2\},$

$\{a \mapsto 1, b \mapsto 1\}, \{a \mapsto 1, b \mapsto 2\},$

$\{a \mapsto 2, b \mapsto 1\}, \{a \mapsto 2, b \mapsto 2\} \}$

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 $m = \{a \mapsto 1, b \mapsto 3, c \mapsto 5, d \mapsto 7\}$ then $dom m = {a, b, c, d}$ , $rng m = {1,3,5,7}$ , m(a) = 1, m(b) = 3, etc.

[edit] Map Overriding

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

$m_1 = \{a \mapsto 1, b \mapsto 2\}$

$m_2 = \{a \mapsto 2, c \mapsto 2\}$

then $m_1 \dagger m_2 = \{a \mapsto 2, b \mapsto 2, c \mapsto 2\}$ .

[edit] Bank system example

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

B a n k ::

$accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData$

$overdraftMap : CustNum \begin{matrix} m \ o \end{matrix} Overdraft$

where

$inv\mbox{-}Bank(mk\mbox{-}Bank(accountMap, overdraftMap))\underline{\Delta}$

$\quad \forall mk\mbox{-}AccData(CustNum, balance) \in\mbox{ rng } AccNum \ \bullet$

$\quad CustNum \in \mbox{ dom } overdraftMap \land balance \ge -overdraftMap(CustNum)$

A c c D a t a ::

o w n e r : C u s t N u m

b a l a n c e : B a l a n c e

$Overdraft = \mathbb{N}$

$Balance = \mathbb{Z}$

With operations: NEWC allocates a new customer number:

N E W C (o d : O v e r d r a f t) r : C u s t N u m

$\mbox{ext wr }odm : CustNum \begin{matrix} m \ o \end{matrix} Overdraft$

$\mbox{post }r \notin \mbox{ dom } \begin{matrix}\leftharpoonup \\ overdraftMap \end{matrix} \land overdraftMap = \begin{matrix}\leftharpoonup \\ overdraftMap \end{matrix} \dagger \{r \mapsto od\}$

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

N E W A C (c u : C u s t N u m) r : A c c N u m

$\mbox{ext rd } overdraftMap : CustNum \begin{matrix} m \ o \end{matrix} Overdraft$

$\quad \mbox{wr } accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData$

pre c u e dom o v e r d r a f t M a p

$\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)\}$

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

$ACINF(cu : CustNum)r : AccNum \begin{matrix} m \ o \end{matrix} Balance$

$\mbox{ext rd } accountMap : AccNum \begin{matrix} m \ o \end{matrix} AccData$

$\mbox{post } r = \{AccNum \mapsto balance(accountMap(AccNum)) |$

$\quad \quad AccNum e \mbox{ dom } accountMap \land owner(accountMap(AccNum)) = cu\}$

[edit] 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 $a, b, c \in X$ . The empty sequence is [].

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

[edit] Sequence operations

VDL-SL has the following sequence operations:

$hd _$	$\ : X^* \rightarrow X$	head (first element)
$lt _$	$\ : X^* \rightarrow X^*$	tail (remainder)
$len _$	$\ : X^* \rightarrow \mathbb{N}$	length
$elems _$	$\ : X^* \rightarrow X\mbox{-set}$	set of elements
$_(_)$	$\ : X^* \times \mathbb{N}_1 \rightarrow X$	element selection
$_(c u r v e a r r o w)_$	$\ : X^* \times X^* \rightarrow X^*$	concatenation

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

[edit] Examples

[edit] The max function

$max(i : \mathbb{Z}, j : \mathbb{Z})r : \mathbb{Z}$

$pre\ true$

$post (r = i \lor r = j) \land i \le r \land j \le r$

[edit] Natural number multiplication

$multp(i : \mathbb{N}, j : \mathbb{N})r : \mathbb{N}$

$pre\ true$

$post\ r = i*j$

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

$multp(i,j) \underline{\triangle}$

$\mbox{if}\ i=0$

$\mbox{then}\ 0$

$\mbox{else if}\ is\mbox{-}even(i)$

$\mbox{then}\ 2*multp(i/2,\ j)$

$\mbox{else}\ j + multp(i-1,\ j)$

Then the proof obligation becomes:

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

This can be shown correct by the following steps:

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

[edit] Mathematical operators

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

$\_ + \_ : \mathbb{Z} \times \mathbb{Z} \to \mathbb{Z}$
$\_\ mod\ \_ : \mathbb{N} \times \mathbb{N}_1 \to \mathbb{N}$	Note that unlike most porgramming languages, VDM does not allow the negative operands for the mod operator
$\_\ divides\ \_ : \mathbb{N}_1 \times \mathbb{N} \to \mathbb{B}$
$i\ divides\ j\ \underline{\triangle}\ j\ mod\ i = 0$

[edit] Queue abstract data type

types

Q e l t = To Be Defined

Q u e u e = Q u e l t *

state T h e Q u e u e of

q : Q u e u e

end

operations

E N Q U E U E (e : Q e l t)

ext wr q : Q u e u e

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

D E Q U E U E () e : Q e l t

ext wr q : Q u e u e

$\mbox{pre }q \ne []$

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

$IS\mbox{-}EMPTY() r : \mathbb{B}$

ext rd q : Q u e u e

$\mbox{post }r \Leftrightarrow (\mbox{len }q = 0)$

[edit] See also

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

[edit] External links

VDM standard

[edit] References

D. Bjørner and C. B. Jones (eds.), The Vienna Development Method: The Meta-Language, Lecture Notes in Computer Science, Vol. 61, Springer-Verlag 1978. ISBN 0-387-08766-4
D. Bjørner and C. B. Jones, Formal Specification and Software Development Prentice Hall International, 1982. ISBN 0-13-880733-7
J. Dawes, The VDM-SL Reference Guide, Pitman 1991. ISBN 0-273-03151-1
J. S. Fitzgerald and P. G. Larsen, Modelling Systems: Practical Tools and Techniques for Software Development, Cambridge University Press, 1998, ISBN 0-521-62348-0
J. S. Fitzgerald, P. G. Larsen, P. Mukherjee, N. Plat and M. Verhoef. Validated Designs for Object-oriented Systems, Springer-Verlag, 2005. ISBN 1-85233-881-4
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 0-13-880725-6
C. B. Jones, Software Development: A Rigorous Approach, Prentice Hall International, 1980. ISBN 0-13-821884-6
C. B. Jones and R. Shaw (eds.), Case Studies in Systematic Software Development, Prentice Hall International, 1990. ISBN 0-13-880733-7

This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.

Retrieved from "http://en.wikipedia.org../../../v/d/m/VDM_specification_language_c910.html"

Categories: Cleanup from March 2006 | Articles to be merged since November 2006 | FOLDOC sourced articles | Formal specification languages