🚀 go-pugleaf

:: Rapid prototyping of Z specifications ::

A student project this year in the Department of Computer Science at
the University of Edinburgh will involve producing a functional
programming language testbed for Z specifications.

Z specifications are, of course, not conventionally executable and
must be refined to implementations in conventional programming
languages.  This development process produces proof obligations some
parts of which (e.g. base cases in inductive proofs) may be discharged
by testing an obvious refinement of the specification.  The purpose of
this project would be to make the construction of obvious refinements
relatively easy by the provision of an implementation of the datatypes
and operators of the Z basic library in a programming language such as
(the functional subset of) Standard ML.  This testbed would assist
software developers who wish to prototype their formal specifications
of software systems.

I would like to hear of relevant work in this area.  I am familiar
with the literature on this topic which has been presented at Z User
Meetings or is widely known in the community.

I would also like to recruit volunteers who are willing to test a
prototype implementation of the testbed due to be released early in
1992 and who would be willing to report their experience by mid-1992
in time for examination of the project.  The only software which will
be necessary to use the testbed is likely to be the Standard ML
programming language which is available free or for a nominal sum from
a number of software archives or academic sites.

Software developers who have now or will have at that time a small
specification which could be prototyped as a case study in the project
should also make contact.


Stephen Gilmore

Laboratory for Foundations of      JANET: stg@uk.ac.ed.lfcs
  Computer Science                 UUCP:  ..!mcvax!ukc!lfcs!stg
Department of Computer Science     ARPA:  stg%lfcs.ed.ac.uk@nsfnet-relay.ac.uk
The James Clerk Maxwell Building
The King's Buildings
University of Edinburgh
Edinburgh EH9 3JZ,  UK.            Tel:   (+44) 031-650-5145