Kevin.Lano@prg.oxford.ac.uk (04/24/91)
> 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