stg@cs.ed.ac.uk (Stephen Gilmore) (06/21/91)
:: 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