Editing Vienna Development Method (section)

==Refinement==
Use of VDM starts with a very [[abstraction (computer science)|abstract]] model and develops this into an implementation. Each step involves ''data reification'', then ''operation decomposition''.

Data reification develops the [[abstract data type]]s into more concrete [[data structure]]s, while operation decomposition develops the (abstract) implicit specifications of operations and functions into [[algorithm]]s that can be directly implemented in a computer language of choice.

:<math>\begin{array}{|rcl|}
\textbf{Specification}
& &
\textbf{Implementation}
\\
\hline
\text{Abstract data type} &
\xrightarrow\text{Data reification} &
\text{Data structure}
\\
\text{Operations} &
\xrightarrow[\text{Operation decomposition}]{} &

\text{Algorithms}
\end{array}</math>

===Data reification===
Data reification (stepwise refinement) 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 reification step for an abstract data representation <code>ABS_REP</code> involves proposing a new representation <code>NEW_REP</code>. In order to show that the new representation is accurate, a ''retrieve function'' is defined that relates <code>NEW_REP</code> to <code>ABS_REP</code>, i.e. <code>retr : NEW_REP -> ABS_REP</code>. The correctness of a data reification depends on proving ''adequacy'', i.e.
<syntaxhighlight lang="rsl">
 forall a:ABS_REP & exists r:NEW_REP & a = retr(r)
</syntaxhighlight>
Since the data representation has changed, it is necessary to update the operations and functions so that they operate on <code>NEW_REP</code>.  The new operations and functions should be shown to preserve any data type [[Invariant (computer science)|invariants]] on the new representation. In order to prove that the new operations and functions model those found in the original specification, it is necessary to discharge two proof obligations:
* Domain rule:
<syntaxhighlight lang="rsl">
 forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
</syntaxhighlight>
* Modelling rule:
<syntaxhighlight lang="rsl">
 forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))
</syntaxhighlight>

====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:
* <code>INIT()</code> initialises the system, assumes that the factory is empty
* <code>ENTER(p : Person)</code> records that a worker is entering the factory; the workers' details are read from the ID card)
* <code>EXIT(p : Person)</code> records that a worker is exiting the factory
* <code>IS-PRESENT(p : Person) r : bool</code> checks to see if a specified worker is in the factory or not

Formally, this would be:
<syntaxhighlight lang="rsl">
 types

 Person = token;
 Workers = set of Person;

 state AWCCS of
   pres: Workers
 end

 operations

 INIT()
 ext wr pres: Workers
 post pres = {};

 ENTER(p : Person)
 ext wr pres : Workers
 pre p not in set pres
 post pres = pres~ union {p};

 EXIT(p : Person)
 ext wr pres : Workers
 pre p in set pres
 post pres = pres~\{p};

 IS-PRESENT(p : Person) r : bool
 ext rd pres : Workers
 post r <=> p in set pres~
</syntaxhighlight>
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 (computer science)|invariant]] to the new data type. In this case, ordering is not important, so <code>[a,b]</code> is the same as <code>[b,a]</code>.

The Vienna Development Method is valuable for model-based systems. It is not appropriate if the system is time-based. For such cases, the [[calculus of communicating systems]] (CCS) is more useful.