Editing Vienna Development Method (section)

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