steve@hubcap.clemson.edu ("Steve" Stevenson) (07/26/90)
Does anyone know of the actual use of any formal semantics techniques in describing a common language for which there is a standard (e.g. C, Fortan, Cobol, Pascal) and such description is subsequently used for a commercially available implementation? Thanks -- =============================================================================== Steve (really "D. E.") Stevenson steve@hubcap.clemson.edu Department of Computer Science, (803)656-5880.mabell Clemson University, Clemson, SC 29634-1906
rwh@PROOF.ERGO.CS.CMU.EDU (Robert Harper) (07/27/90)
steve@hubcap.clemson.edu ("Steve" Stevenson) writes: >Does anyone know of the actual use of any formal semantics techniques >in describing a common language for which there is a standard >(e.g. C, Fortan, Cobol, Pascal) and such description is subsequently >used for a commercially available implementation? "The Definition of Standard ML" by Robin Milner, Mads Tofte, and Robert Harper, MIT Press, 1990. There are several implementations, some public-domain (SML/NJ), some commericial products (Abstract Hardware Ltd's SML). The relationship between the formal semantics and an implementation has been a topic of active discussion. -- Robert Harper School of Computer Science Net: rwh@cs.cmu.edu Carnegie Mellon University Phone: +1 412 268 3675 Pittsburgh, PA 15213
cliff@cs.man.ac.uk (Cliff Jones) (07/31/90)
Hi there!
There are several VDM definitions of standard languages. The Bjorner/Jones
book (see below) has VDM descriptions of Pascal and ALGOL 60; that has
refernces to the Vienna work which sparked off VDM: a description of
ECMA/ANSI PL/I.
Springer-Verlag's LNCS 98 reports on early attempts by the DDC to
describe Ada. A version of this was then used in their development of
an Ada compiler (the first European compiler to be approved via the
DoD test cases I believe). There was subsequent ESPRIT-funded work to
develop a full Ada semantics.
The current Modula-2 standard is being developed in VDM.
cliff jones
========================================
@book{BjornerJones82,
author = "D. Bj{\o}rner and C.B. Jones",
year = "1982",
publisher = "Prentice Hall International",
title = "Formal Specification and Software Development",
note = "501 pages"
}
@BOOK{ Bjorner80f,
EDITOR = "D. Bj{\o}rner and O.Oest",
TITLE = "Towards a Formal Description of {Ada}",
PUBLISHER = S-V,
YEAR = "1980",
VOLUME = "98",
SERIES = LNCS
}