Path: utzoo!utgpu!watmath!clyde!ima!compilers-sender From: frode@m2cs.naggum.se (Frode Odegard) Newsgroups: comp.compilers Subject: Re: Why Can't We Build a C Compiler? Summary: Modula-2 also has a formal semantic definition Message-ID: <3112@ima.ima.isc.com> Date: 29 Dec 88 11:26:08 GMT References: <3099@ima.ima.isc.com> Sender: compilers-sender@ima.ima.isc.com Reply-To: Frode Odegard Organization: Modula-2 CASE Systems A.S, Oslo, Norway Lines: 26 Approved: compilers@ima.UUCP In article <3099@ima.ima.isc.com>, nick@lfcs.ed.ac.uk (Nick Rothwell) writes: > This is the approach we've taken with the ML project. Standard ML is, > to my knowledge, the only language to have a complete formal semantics ... > (which is *not* huge - 97 pages). Does Ada have one? How big is it In the upcoming ISO standard for Modula-2, VDM is used to define the semantics [as well as the syntax]. This will increase the safety of compilers. In England they are working on a system which will produce and prove a compiler for a language specified in VDM [I think this is in connection with the Alvey-project]. I expect that there is and will be serious work done on proving Modula-2 programs, taking advantage of the fact that the language is defined in VDM. BTW, I think a VDM standard is on its way :-) - Frode Odegard, M2CS PS: I think the worst "hack" in the VDM definition of Modula-2 is how continuity is handled in connection with coroutines. I heard that the VDM ";" combinator is being overloaded ;-> I'm not sure this is really a "hack"....my VDM stinks. [From Frode Odegard ] -- Send compilers articles to ima!compilers or, in a pinch, to Levine@YALE.EDU Plausible paths are { decvax | harvard | yale | bbn}!ima Please send responses to the originator of the message -- I cannot forward mail accidentally sent back to compilers. Meta-mail to ima!compilers-request