Xref: utzoo comp.software-eng:4361 comp.specification:175
Path: utzoo!attcan!uunet!mcsun!ukc!mucs!cliff
From: cliff@cs.man.ac.uk (Cliff Jones)
Newsgroups: comp.software-eng,comp.specification
Subject: Re: Formal specifications of Pascal
Message-ID: <1827@m1.cs.man.ac.uk>
Date: 24 Oct 90 17:57:05 GMT
References: <2317@charon.cwi.nl> <6698@castle.ed.ac.uk>
Sender: news@cs.man.ac.uk
Reply-To: cliff@cs.man.ac.uk (Cliff Jones)
Followup-To: comp.software-eng
Organization: Department of Computer Science, University of Manchester UK
Lines: 36

In article <6698@castle.ed.ac.uk> sean@castle.ed.ac.uk (S Matthews) writes:
>arie@cwi.nl (Arie v. Deursen) writes:
...
>In the book by C. B. Jones and D. Bjorner published in Prentice Hall
>International there are are a large number of case studies, one of which
>is a formal semantics of Pascal written in (an old version of ) VDM.
>It gives the whole semantics though.
>
>It is big and ugly, especially compared to the definition of Algol-60
>which is also given.  A good argument against at least parts of
>Pascal.

It is interesting to look at this comparison (I'm fairly sure that the
fact that *both* definitions are in VDM ("old version thereof") does
not influence the comparison).

The context conditions (static semantics) is likely to be bigger just
because Pascal has a "richer" type structure than ALGOL60. I think
that most people would prefer a language to records with one without;
I hope most people would be happier if the types were checked statically.

The size of the (dynamic) semantics is more worrying. I talked a lot
to Derek Andrews when he was trying to work from the ALGOL definition
towards that for Pascal. Several times it was *very tempting* to "clean
up" the language and I argued that Pascal should be described "warts
and all". One (bad) example that I remember was the way that Pascal
permits variant records *and* allows untagged VRs to be passed by
location. The *combination* of these features adds to the size and
"ugliness" of the definition.

I guess my reason for going through this is to hammer home the point
(as put well in - for example - Schmidt's book) that formal
models/descriptions should be constructed as a language is designed
*not* as post facto exercises.

cliff jones