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
arie@cwi.nl (Arie v. Deursen) (10/26/90)
Dear reader,
I`ve received several responses on my question for formal specifications of
the static semantics for Pascal. I'd like to thank everybody who gave a
response.
It really helped me.
Since there is still some discussion in this group on the subject, and
since several others may be interested as well, I'll post a summary:
Summarized:
1. ISO International Standard, programming languages, Pascal, ISO
7185-1983 (E)
2. U. Kastens, B. Hutt, E. Zimmermann, GAG: A Practical Compiler Generator,
Lecture Notes in Computer Science 141, Springer-Verlag, 1982
Martin Weigele:
3. An axiomatic definition of Pascal, Acta Informatica 2, 335-355, 1973
Marie-Laure Potet, Stephen J. Bevan, Michael Dyck, Matthys Kuiper:
4. David a. Watt, An Extended Attribute Grammar for Pacal, SIGPLAN Notices,
Vol. 14, No 2, 1979, pp 60--74
Matthys Kuiper:
5. Mim Welsh & Atholl Hay, A model Implementation of Standard Pascal
Theo Norvell:
For languages similar to Pascal check out:
6. Wolfgang Pollak's thesis (published as a LNCS by Springer-Verlag)
7. The Design and Definition of the Turing Programming Language, by
Holt et al,
published by Prentice-Hall.
Bruce T. Forstall:
8. Reps & Teitlebaum's Synthesizer Generator (formerly, the Cornell Program
Synthesizer) is a syntax-directed editor generator that uses an
incrementally updated attribute grammar for static semantics.
There are several books and papers describing the system. They have a
complete attribute description of Pascal, that might even do code
generation.
9. In Robert Ballance's PhD thesis--"Syntactic and Semantic Checking in
Language- Based Editing Systems"--he describes ``logical constraint
grammars,'' which resemble Prolog descriptions, for describing language
semantics. This is Technical report UCB/CSD 89/548, from UC Berkeley's
Computer Science Division. He references other semantic analysis systems.
Sean Matthews, Stephen J. Bevan, Michael Dyck, Cliff Jones:
10. @BOOK{BjornerJones82,
AUTHOR = {Dines Bj{\o}rner and Cliff B. Jones},
TITLE = {Formal Specification \& Software Development},
PUBLISHER = {Prentice Hall International},
YEAR = {1982},
SERIES = {Computer Science}
}
Sean Matthews:
11. Another place to look for references would be Mike Gordon's book by the
same publisher.
Paul Sander (paul@Atherton.COM):
12. Pascal User Guide and Report, N. Wirth, Kathleen Jensen, Springer-Verlag
Thank you all,
Arie
CWI, P.O. Box 4079 Arie van Deursen (arie@cwi.nl)
1009 AB Amsterdam
The Netherlands Ich weiss nicht was soll es bedeuten ...
Tel. 31 20 5924007