🚀 go-pugleaf

> Has anyone used Z to define the static semantics of a ``normal''
> language (pascal, Modula-2,...)? Any reason why it would be 
> more difficult than using VDM? I'd appreciate any references
> to the literature.
 
Chris
collberg@dna.lth.se
 
I am currently writing a specification of (part of) 
the semantics for COBOL 74 in Z. This is a 
denotational semantics, and Z is quite a reasonable 
language to use to specify this. All one needs is 
the lambda calculus - although a more elegant way of 
defining retracts, recursive Scott domains, would be 
useful. 
 
Related documents are available from the REDO project
at Oxford. The way we made the task managable was to 
translate COBOL to a simpler intermediate language, 
and specify that, rather than dealing with the whole 
of COBOL (300+ keywords). Finding out what the obscure
features of the language actually did was another 
problem. 
 
The paper ``From Code to Z specifications", Z User
Meeting 1989, deals in part with this task. 
 
Kevin Lano