Editing Vienna Development Method (section)

====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.