Information Technology Reference
In-Depth Information
A different and more general problem with providing online access to large
VDM specifications is to allow ecient searching for particular items of interest.
For semantic descriptions of programming languages, it would be useful to search
for the parts concerning particular (concrete or abstract) constructs. Searching
for mathematical formulae is inherently dicult, and addressed on the web by
using special markup languages such as MathML; but this would not help with
existing, older documents. A possible solution might be to add bookmarks to
pdfs, identifying the pages concerned with particular constructs.
There is also the issue of copyright. Presumably all authors of semantic de-
scriptions would be happy to see their work made accessible online, but some
publishers are unlikely to agree to free access. A compromise might be to provide
free access only to summary information about semantic descriptions, sucient
to support searching for descriptions of particular constructs, but require login
as a registered user to see the pdf of the description itself.
The author is currently investigating the possibility of establishing a repos-
itory for semantic descriptions of programming languages in all major frame-
works; VDM would be among the first to be covered. Readers who have copies
of significant semantic descriptions of programming languages (in any format)
are kindly requested to contact the author, indicating what they could provide,
and who holds the copyright.
7Conluon
The fundamental principles of denotational semantics were established by Scott
and Strachey at Oxford in the early 1970s. VDM adopted these principles, but
also introduced some innovations: in particular, VDM made much greater use
of combinators than was usual in the original Oxford style. Significantly, each
combinator in VDM has a fixed operational interpretation, whereas its definition
in λ -notation can vary; see also [33]. We have seen that some of the VDM
combinators introduced in the early 1970s correspond directly to operations
provided in the monadic style of denotational semantics, which was developed
at the end of the 1980s; moreover, the way their definitions vary corresponded
to the lifting of operations by particular monad transformers.
VDM semantic descriptions of some major programming languages have been
published, including PL/I, Algol 60, Pascal, Ada, and Modula-2. They are valu-
able sources of examples of how to describe a wide range of programming con-
structs using VDM, and deserve to be much more easily accessible to researchers
and students than at present; including them in the proposed online repository
of semantic descriptions would not only make them electronically available, but
should also allow searching for descriptions of particular kinds of constructs.
Acknowledgement. Thanks to Cliff Jones and Eugenio Moggi for helpful com-
ments on drafts of this paper, and to the organisers for the invitation to give a
presentation at the symposium.
This paper was written in celebration of Dines Bjørner's 70th birthday. As one
of the originators of VDM, through his many articles and topics about VDM,
 
Search WWH ::




Custom Search