Xref: utzoo comp.software-eng:4286 comp.specification:155
Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!wuarchive!uunet!mcsun!ukc!edcastle!sean
From: sean@castle.ed.ac.uk (S Matthews)
Newsgroups: comp.software-eng,comp.specification
Subject: Re: Formal specifications of Pascal
Keywords: Formal Specifications, Pascal, Algebraic Specifications
Message-ID: <6698@castle.ed.ac.uk>
Date: 12 Oct 90 13:44:57 GMT
References: <2317@charon.cwi.nl>
Organization: Edinburgh University Computer Services
Lines: 27

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