Information Technology Reference
In-Depth Information
Ada:
A VDM semantics for full Ada was initially developed by Dines Bjørner and
several MSc students under his supervision at the Danish Technical University,
and published as a volume of LNCS with the title
Towards a Formal Description
of Ada
in 1980 [26]. This description was subsequently revised and finalised
in a series of technical reports, published by Dansk Datamatik Center (DDC)
in 1981-2, which provided the basis for the rigorous development of an Ada
compiler [27]. The compiler was released in 1983, and became renowned not
only for its quality, but also as commercially successful. The unqualified success
of this application of VDM was a clear vindication of Dines Bjørner's trust in
the suitability of the VDM specification language for describing the semantics of
large languages such as Ada, as well as a welcome, highly visible demonstration
of the potential usefulness of research in formal semantics.
VDM was later used also in the ocial
Draft Formal Definition of Ada
, but
only for the static semantics [28]. The dynamic semantics [29,30] was specified
using SMoLCS [31], which uses a “VDM-like” style of denotational semantics to
map Ada programs into a semantic algebra, where behaviour (including concur-
rency) is specified using a combination of labelled transition rules and algebraic
axioms. The semantic algebra includes the combinators used in VDM.
Modula-2:
VDM was used, along with English text, for defining the semantics
of Modula-2 in the ISO/IEC base standard, which was developed from 1987 to
1996. The formal definition and the English text are regarded as having equal
importance. According to an article about the process of producing the standard
[20], it contains about “200 type definitions, 1800 function and operation defin-
itions and some 20,000 lines of VDM-SL code”. All the VDM-SL specifications
were “tested for syntactical accuracy and semantic constraints” using a front
end for VDM-SL developed at Delft University of Technology. ISO/IEC did not
allow publication of the standard on the web [32], although a draft version is
available.
5
Online access:
The VDM Portal
6
provides online access to many VDM docu-
ments, including examples of specifications in VDM-SL and VDM++. However,
it appears that only
two
VDM semantic descriptions of programming languages
are currently available through the portal: one for a language called
NewSpeak
from 1994, the other for a tutorial-style example of static and dynamic semantics
of a simple programming language.
One problem with providing online access to the VDM semantic descriptions
cited above is that they are generally available only in printed form, and would
need scanning to pdf (fortunately, this has already been done for parts of the
PL/I semantics [17] - although it is frustrating not to have access to the rest
of it at present - and for the semantics of Algol 60 and Pascal in [18]). It is
conceivable that the original sources of some of the documents have been archived
electronically, in which case it might be feasible to retrieve them and use them
to generate searchable pdfs.
Search WWH ::
Custom Search