Specifying static semantics in Z

Thread View: comp.specification

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by Kevin.Lano Wed, 24 Apr 1991 09:29

#369

Author: Kevin.Lano
Date: Wed, 24 Apr 1991 09:29

29 lines
1410 bytes

> 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

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads