Editing Vienna Development Method (section)

==Modelling functionality==
===Functional modelling===
In VDM-SL, functions are defined over the data types defined in a model. Support for abstraction requires that it should be possible to characterize the result that a function should compute without having to say how it should be computed. The main mechanism for doing this is the ''implicit function definition'' in which, instead of a formula computing a result, a logical predicate over the input and result variables, termed a ''postcondition'', gives the result's properties. For example, a function <code>SQRT</code> for calculating a square root of a natural number might be defined as follows:
<syntaxhighlight lang="rsl">
SQRT(x:nat)r:real
post r*r = x
</syntaxhighlight>
Here the postcondition does not define a method for calculating the result <code>r</code> but states what properties can be assumed to hold of it. Note that this defines a function that returns a valid square root; there is no requirement that it should be the positive or negative root. The specification above would be satisfied, for example, by a function that returned the negative root of 4 but the positive root of all other valid inputs. Note that functions in VDM-SL are required to be ''deterministic'' so that a function satisfying the example specification above must always return the same result for the same input.

A more constrained function specification is arrived at by strengthening the postcondition. For example, the following definition constrains the function to return the positive root.
<syntaxhighlight lang="rsl">
SQRT(x:nat)r:real
post r*r = x and r>=0
</syntaxhighlight>
All function specifications may be restricted by ''preconditions'' which are logical predicates over the input variables only and which describe constraints that are assumed to be satisfied when the function is executed. For example, a square root calculating function that works only on positive real numbers might be specified as follows:
<syntaxhighlight lang="rsl">
SQRTP(x:real)r:real
pre x >=0
post r*r = x and r>=0
</syntaxhighlight>
The precondition and postcondition together form a ''contract'' that to be satisfied by any program claiming to implement the function. The precondition records the assumptions under which the function guarantees to return a result satisfying the postcondition. If a function is called on inputs that do not satisfy its precondition, the outcome is undefined (indeed, termination is not even guaranteed).

VDM-SL also supports the definition of executable functions in the manner of a functional programming language. In an ''explicit'' function definition, the result is defined by means of an expression over the inputs. For example, a function that produces a list of the squares of a list of numbers might be defined as follows:
<syntaxhighlight lang="rsl">
SqList: seq of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)
</syntaxhighlight>
This recursive definition consists of a function signature giving the types of the input and result and a function body. An implicit definition of the same function might take the following form:
<syntaxhighlight lang="rsl">
SqListImp(s:seq of nat)r:seq of nat
post len r = len s and
     forall i in set inds s & r(i) = s(i)**2
</syntaxhighlight>
The explicit definition is in a simple sense an implementation of the implicitly specified function. The correctness of an explicit function definition with respect to an implicit specification may be defined as follows.

Given an implicit specification:
<syntaxhighlight lang="rsl">
f(p:T_p)r:T_r
pre pre-f(p)
post post-f(p, r)
</syntaxhighlight>
and an explicit function:
<syntaxhighlight lang="rsl">
f:T_p -> T_r
</syntaxhighlight>
we say it satisfies the specification [[iff]]:
<syntaxhighlight lang="rsl">
forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))
</syntaxhighlight>
So, "<code>f</code> is a correct implementation" should be interpreted as "<code>f</code> satisfies the specification".

===State-based modelling===
In VDM-SL, functions do not have side-effects such as changing the state of a persistent global variable. This is a useful ability in many programming languages, so a similar concept exists; instead of functions, ''operations'' are used to change '''state variables''' (also known as ''globals'').

For example, if we have a state consisting of a single variable <code>someStateRegister : nat</code>, we could define this in VDM-SL as:
<syntaxhighlight lang="rsl">
 state Register of
   someStateRegister : nat
 end
</syntaxhighlight>
In VDM++ this would instead be defined as:
<syntaxhighlight lang="rsl">
 instance variables
   someStateRegister : nat
</syntaxhighlight>
An operation to load a value into this variable might be specified as:
<syntaxhighlight lang="rsl">
 LOAD(i:nat)
 ext wr someStateRegister:nat
 post someStateRegister = i
</syntaxhighlight>
The ''externals'' clause (<code>ext</code>) specifies which parts of the state can be accessed by the operation; <code>rd</code> indicating read-only access and <code>wr</code> 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:
<syntaxhighlight lang="rsl">
 ADD(i:nat)
 ext wr someStateRegister : nat
 post someStateRegister = someStateRegister~ + i
</syntaxhighlight>
Where the <code>~</code> symbol on the state variable in the postcondition indicates the value of the state variable before execution of the operation.