Semantic descriptions library
These are my (current, evolving) contributions to Peter Mosses's
"library of semantics".
VDM descriptions of programming languages
Those aspects of "VDM" relating to language description were firmed up in the IBM Laboratory in Vienna
around a project to build a complier from the PL/I language to the "FS" machine (that got cancelled).
One direct output was "published" as the Technical Report on the
PL/I description
which I've had scanned;
full citation
Another report described the
overall method
full citation
An older report investigated different
implementation techniques for reference to non-local variables
(Warning: this uses VDL notation!)
full citation
Other descriptions (follow the citation links to get to the pdf)
using VDM include:
An interesting precursor of the shift to denotational semantics
was a "functional semantics" written between my two stays in Vienna
(1968--70, 1973--76)
- This IBM Hursley Technical Report TR12.105
contains a semantics of ALGOL-60 (the standard challenge language).
We decided to print (in Section 5) the ALGOL report on right-hand pages facing the relevant formulae
on left hand pages;
printed landscape!!
The best approximation that I can give to this is to print two landscape pages above each other on A4.
(A further warning is that since this was scanned, the pdf is over 5Mb.)
Technically the material has some residual interest because it works out the "exit" idea
in a framework that is related to Plotkin's SOS --- but my notation was verbose.
Linking in the other direction,
having done this it was easy to absorb the "exit combinators" into the denotational VDM.
Related (Programming language description) VDM on-line resources
(follow the citation links to get to the pdf)
VDM for general program specification/design
See
VDM
Cliff's Home