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

λβ 1 .Assign ( β 0 | λρ.λθ. E [[ ε 0 ]] ( ρ ) { λβ 0 . E [[ ε 1 ]] ( ρ ) { L, β 1 ) }}

λβ 1 .Assign ( β 0 | = λρ. E [[ ε 0 ]] ( ρ ) ◦ λβ 0 . E [[ ε 1 ]] ( ρ ) ◦ L, β 1 ) (14)

where Assign : L × V → C → C is the continuation-passing version of Assign .

for avoiding deeply-nested braces is to introduce
an infix combinator corresponding to application, but grouping to the right.
Tennent [12] and Gordon [13] used semicolons for this purpose, writing e.g.:

An alternative to the use of ◦

C [[ γ 0 ; γ 1 ]] = λρ.λθ. C [[ γ 0 ]] ( ρ ); C [[ γ 1 ]] ( ρ ); θ (15)

4TheVDMS y e

This section focusses on the distinctive features of the VDM style of denotational
semantics, which was already quite stable by 1974 [17]. The illustrations and ex-
planations given here are based primarily on the presentation of VDM in the
book by Dines Bjørner and Cliff Jones from 1982 [18], since it is essentially that
version of the VDM specification language, known as Meta-IV , which has been
used for almost all published VDM semantic descriptions of major programming
languages (see Sect. 6 for references). A subsequent version, VDM-SL , was stan-
dardised by ISO in 1996 [19], and was used for defining the formal semantics
of Modula-2 in its ISO standard [20]. Although there may be some significant
differences between Meta-IV and VDM-SL , the combinators provided appear to
be very similar. Caveat: The author has not followed the development of VDM
at all closely since the end of the 1980s, and the explanations below should
definitely not be regarded as authoritative.
In contrast to the Oxford style of denotational semantics, illustrated in the
previous section, the VDM style is quite verbose, generally using (abbreviated)
English words rather than single letters and mathematical signs. Another styl-
istic difference is that in VDM, the notation used for abstract syntax (inherited
from VDL) does not involve the concrete symbols of the described language.
The VDM style is clearly more appropriate than the Oxford style for describing
larger programming languages.

4.1 Abstract Syntax

The VDM style of specifying abstract syntax is illustrated in Fig. 2. The absence
of terminal symbols from the concrete syntax of the described language makes
the mapping from program texts to abstract syntax trees somewhat less obvious
than in the Oxford style, but the words used as nonterminal symbols in the
abstract syntax are usually quite suggestive, and in practice it is not dicult to
imagine the exact relationship to a concrete syntax.
Another difference from the Oxford style is that the nonterminal symbols
of the abstract grammar are the names of the sets of abstract syntax trees
themselves, rather than metavariables over those sets. Moreover, VDM requires
a separate nonterminal to be introduced for each kind of statement, expression,
etc. A grammar rule of the form N=N1 | ... | Nm defines N to be the union