arie@cwi.nl (Arie v. Deursen) (10/11/90)
Hello, I am looking for literature concerning formal specifications for the static semantics of Pascal. The static semantics of a strongly typed language like Pascal, mainly covers, of course, its type checking rules. I am very interested in formal specifications for the type check rules for Pascal. I already have studied the ISO standard (ISO 7185): natural language, not very formal mathematically spoken, and I have looked at the attributed grammar definition of the GAG system, by Uwe Kastens c.s. (LNiCS 141). I would appreciate any help, thanks in advance, Arie Arie van Deursen Centrum voor Wiskunde en Informatica (CWI) (arie@cwi.nl) P.O. Box 4079, 1009 AB Amsterdam, The Netherlands
sean@castle.ed.ac.uk (S Matthews) (10/12/90)
arie@cwi.nl (Arie v. Deursen) writes: es >Hello, >I am looking for literature concerning formal specifications for the static >semantics of Pascal. The static semantics of a strongly typed language like >Pascal, mainly covers, of course, its type checking rules. >I am very interested in formal specifications for the type check rules >for Pascal. >Arie van Deursen Centrum voor Wiskunde en Informatica (CWI) >(arie@cwi.nl) P.O. Box 4079, 1009 AB Amsterdam, The Netherlands 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. Another place to look for references would be Mike Gordon's book by the same publisher. Sean Matthews
cliff@cs.man.ac.uk (Cliff Jones) (10/18/90)
You ask for a (static) semantics of Pascal. This is covered in the
Andrews/Henhapl chapter in:
@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"
}
cliff jonescliff@cs.man.ac.uk (Cliff Jones) (10/25/90)
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