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

PL/I: The technical report A Formal Definition of a PL/I Subset by Hans Bekic,
Dines Bjørner, Wolfgang Henhapl, Cliff Jones, and Peter Lucas was published by
the IBM Laboratory in Vienna in 1974 [17]. Covering 201 pages, its length was
modest compared to the size of the language described (and to that of the earlier
definition of PL/I given in the operational VDL framework). The described
subset is essentially the version of PL/I described in the ECMA/ANSI standard
(which does not include tasking) but omitting Input/Output. Section 4 of the
chapter on Notation introduces and defines the VDM combinators concerned
with state transformations, imperative variables, exit, and arbitrary ordering.
Although the original technical report is out of print, 61 pages from it were
reprintedinavolumeofLNCScontaining a selection of papers by Hans Bekic,
and is available online in pdf [17]. The development of a compiler based on the
semantic description stopped in 1975, when IBM cancelled the project to build
the intended target machine [2].
Algol 60: A VDM semantics for Algol 60 by Wolfgang Henhapl and Cliff Jones
was published as Chapter 6 of the topic Formal Specification and Software De-
velopment in 1982 [23]; it is a revision of a previous paper by the same authors
published in the 1978 LNCS volume on VDM [24]. In 33 pages it specifies the
abstract syntax and semantics of the language described in the 1975 Modified
Report on Algol 60, and provides a list of abbreviations as well as an index of
object and function definitions. The specifications of the abstract syntax, static
semantics and dynamic semantics are interleaved, so that the static and dynamic
semantics for the same construct are given close to each other.
The definition of the arbitrary order of evaluation allowed by Algol 60 is delib-
erately not addressed; a few other minor deviations from the intended semantics
of Algol 60 are indicated in comments. Neither the concrete syntax nor its trans-
lation to the abstract syntax are given, although some of the comments refer to
various expansions made by “the translator”.
Pascal: A VDM semantics for Pascal by Derek Andrews and Wolfgang Henhapl
was published as Chapter 7 of the topic Formal Specification and Software De-
velopment in 1982 [25]. As with the VDM semantics for Algol 60 that it follows,
it is a revision of a previous paper published in the 1978 LNCS volume on VDM
[24]. After an introduction commenting on various aspects of the VDM seman-
tics of Pascal, it takes 60 pages to specify the abstract syntax and semantics of
the language described in the BSI/ISO Standard for Pascal.
In contrast to the VDM semantics of Algol 60, the specifications of the abstract
syntax, static semantics, and dynamic semantics of Pascal are not interleaved.
The abstract syntax was chosen to be “fairly close” to the concrete syntax of Pas-
cal, making their relationship “more obvious”. The specification of the abstract
syntax is about 6 pages, including some detailed notes about the intended con-
crete to abstract translation (which involves the introduction of fresh identifiers
“not used elsewhere”). The static semantics takes 22 pages, and the dynamic
semantics 30 pages.