VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 494

In the PL/I semantics [17], ' =>V ' is redefined using a disjoint union:

→ STATE × (res V | abn ABNORMAL)
In [18], however, ' =>V ' is redefined somewhat differently:

=>V = STATE ˜

→ × ×

=>V = STATE ˜ STATE [ ABNORMAL ] V

Redefining ' => 'and' =>V ' requires redefinition of all the combinators, but their
operational interpretation and usage in the semantic equations does not change.
In Sect. 5, we shall see that some of the combinators in VDM are closely
related to standard operations of the monads used in the monadic style of deno-
tational semantics. Moreover, the redefinitions required when abrupt termination
is introduced correspond to the so-called lifting of operations when applying the
standard monad transformer for exception-handling (at least with the definition
of ' =>V ' used in the PL/I semantics [17]). Thus it appears that VDM, right
from the start in the early 1970s, was already using significant elements of the
monadic style that was developed by Eugenio Moggi in the late 1980s [21]. We
shall examine this aspect of VDM further in Sect. 5.

4.3 Denotations

The following examples illustrate the use of the most basic VDM combinators
for defining the denotations of the syntactic constructs shown in Fig. 2, which
correspond directly to those used to illustrate the Oxford style in Sect. 3.
As in the Oxford style, denotations of statements (i.e. commands) are func-
tions of environments. The semantic function M maps statements to their
denotations:

M : Stmt -> ENV =>
The same semantic function also maps expressions to their denotations:

M : Expr -> ENV => VALUE

The abbreviations ' => 'and' => VALUE ' indicate that both statements and ex-
pressions are modelled as state transformations. Whether these transformations
involve the possibility of abnormal termination does not need to be specified
until later, since it does not affect how denotations are expressed. However, to
specify the denotations of assignment statements, we shall need to know how
to select the store from a state. This is specified by indicating the name of the
selector function next to the store component of the state:

STATE :: STR :STORE ...
(The elided further components might support input and output.)
The denotation of a compound statement involves combining the denotations
of an arbitrary number of sub-statements, which can be expressed using the
VDM combinator corresponding to a definite iteration:

M[mk-Compound(sl)](env) = for i=1tolen sl do M[sl](env)