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

inspecting the value of a simple variable involves looking up the location to which
the identifier is bound in the environment, then looking up the current value of
that location in the store.

3 The Oxford Style

Strachey established the Programming Research Group in Oxford in 1965. He
was already developing his own approach to semantics [4] (see also [5, Sect. 3.3]).
Following Scott's discovery of a model for the untyped λ -calculus [7] while on sab-
batical at Oxford in 1969, and Strachey's subsequent collaboration with Scott
in the early 1970s [3], the development of denotational semantics accelerated
rapidly. The group led by Strachey shared his firm conviction that the deno-
tational approach would now do for semantics what BNF had done for syntax
(as witnessed by the Algol 60 Report [8]) and that within a few years, all major
programming languages should have been given a denotational semantics.
The distinctive Oxford style of denotational semantics (often referred to sim-
ply as Scott-Strachey semantics) is particularly concise, and has been followed
in many textbooks and articles on semantics, e.g. [9,10,11,12]. The conciseness
facilitates (pencil and paper) proofs about semantic properties and is strongly
favoured by many theoreticians - but unfortunately, it does not appeal much
to practitioners such as compiler writers and programmers. Let us look at some
simple examples, which have been selected to illustrate the use of combinators
in the Oxford style.

3.1 Abstract Syntax

Recall that abstract syntax trees are essentially derivation trees for an abstract
context-free grammar. The Oxford style of specifying abstract syntax, illustrated
in Fig. 1, is to give a simplified BNF-like grammar using the same terminal sym-
bols as in concrete syntax: reserved words, mathematical signs, and separators.
This makes the intended mapping from program texts to abstract syntax trees
rather easy to imagine, even though there is usually some grouping ambiguity.
The nonterminal symbols of the grammar are written as metavariables ranging
over the corresponding sets of abstract syntax trees; metavariables over the same
set are distinguished by subscripts and/or primes. The style of the metavariables
themselves varies considerably: Scott and Strachey [3] used lowercase Greek let-
ters, Bob Tennent [12] and Joe Stoy [11] used uppercase Greek letters, Mike

γ ∈ Cmd commands

ε ∈ Exp expressions

γ ::= dummy | γ 0 ; γ 1 | ε -> γ 0 , γ 1 | ε 0 := ε 1 | ...
ε ::= ...

Fig. 1. Abstract syntax fragment, Oxford style