Editing Vienna Development Method (section)

==Examples==
{{Further|Meta-IV (specification language)}}

===The ''max'' function===
This is an example of an implicit function definition. The function returns the largest element from a set of positive integers:
<syntaxhighlight lang="rsl">
 max(s:set of nat)r:nat
 pre card s > 0
 post r in set s and
      forall r' in set s & r' <= r
</syntaxhighlight>
The postcondition characterizes the result rather than defining an algorithm for obtaining it. The precondition is needed because no function could return an r in set s when the set is empty.

===Natural number multiplication===
<syntaxhighlight lang="rsl">
 multp(i,j:nat)r:nat
 pre true
 post r = i*j
</syntaxhighlight>
Applying the proof obligation <code>forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))</code> to an explicit definition of <code>multp</code>:
<syntaxhighlight lang="rsl">
 multp(i,j) ==
  if i=0
  then 0
  else if is-even(i)
       then 2*multp(i/2,j)
       else j+multp(i-1,j)
</syntaxhighlight>
Then the proof obligation becomes:
<syntaxhighlight lang="rsl">
 forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j
</syntaxhighlight>
This can be shown correct by:
# Proving that the recursion ends (this in turn requires proving that the numbers become smaller at each step)
# [[Mathematical induction]]

===Queue abstract data type===
This is a classical example illustrating the use of implicit operation specification in a state-based model of a well-known data structure. The queue is modelled as a sequence composed of elements of a type <code>Qelt</code>. The representation is <code>Qelt</code> is immaterial and so is defined as a token type.
<syntaxhighlight lang="rsl">
 types

 Qelt = token;
 Queue = seq of Qelt;

 state TheQueue of
   q : Queue
 end

 operations

 ENQUEUE(e:Qelt)
 ext wr q:Queue
 post q = q~ ^ [e];

 DEQUEUE()e:Qelt
 ext wr q:Queue
 pre q <> []
 post q~ = [e]^q;

 IS-EMPTY()r:bool
 ext rd q:Queue
 post r <=> (len q = 0)
</syntaxhighlight>
===Bank system example===
As a very simple example of a VDM-SL model, consider a system for maintaining details of customer bank account. Customers are modelled by customer numbers (''CustNum''), accounts are modelled by account numbers (''AccNum''). The representations of customer numbers are held to be immaterial and so are modelled by a token type. Balances and overdrafts are modelled by numeric types.
<syntaxhighlight lang="rsl">
 AccNum = token;
 CustNum = token;
 Balance = int;
 Overdraft = nat;

 AccData :: owner : CustNum
            balance : Balance

 state Bank of
   accountMap : map AccNum to AccData
   overdraftMap : map CustNum to Overdraft
 inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                         a.balance >= -overdraftMap(a.owner)
</syntaxhighlight>
With operations:
''NEWC'' allocates a new customer number:
<syntaxhighlight lang="rsl">
 operations
 NEWC(od : Overdraft)r : CustNum
 ext wr overdraftMap : map CustNum to Overdraft
 post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};
</syntaxhighlight>
''NEWAC'' allocates a new account number and sets the balance to zero:
<syntaxhighlight lang="rsl">
 NEWAC(cu : CustNum)r : AccNum
 ext wr accountMap : map AccNum to AccData
     rd overdraftMap map CustNum to Overdraft
 pre cu in set dom overdraftMap
 post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}
</syntaxhighlight>
''ACINF'' returns all the balances of all the accounts of a customer, as a map of account number to balance:
<syntaxhighlight lang="rsl">
 ACINF(cu : CustNum)r : map AccNum to Balance
 ext rd accountMap : map AccNum to AccData
 post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}
</syntaxhighlight>