EPSRC logo

Details of Grant 

EPSRC Reference: GR/L57913/01
Title: IMPLEMENTING CONSTRUCTIVE Z
Principal Investigator: Turner, Professor R
Other Investigators:
Sanderson, Dr M Henson, Professor M C Cardell-Oliver, Dr R
Researcher Co-Investigators:
Project Partners:
Department: Computer Sci and Electronic Engineering
Organisation: University of Essex
Scheme: Standard Research (Pre-FEC)
Starts: 01 January 1998 Ends: 31 March 2001 Value (£): 228,383
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:  
Summary on Grant Application Form
The Z notations is one of the major paradigms in the documentation, design and development of software. If the Z notation has a weakness that prevents wider use it is its ability to bridge the gap from specifications to correct programs. Its high level, set theoretic perspective is excellent for framing abstract specifications but this abstraction, coupled with a lack of theoretical support, hinders a methodical transition to code. The aim of this project is to strengthen and simplify the means by which correct programs may be constructed from standard Z specifications. We propose a new method for software development which integrates Z with the proofs-as-programs development method. Z specifications are interpreted in a new constructive set theory, CZ. We then apply the proofs-as-programs development method to the proofs of CZ specification obligations in order to extract correct programs. Managing proofs and obligations during this process is itself a non-trivial task and requires powerful tool support. We shall build a tool for program development in CZ within the Isabelle prover. The Isabelle theories built for this project will provide both a library of Z specifications and programs together with general, interactive support for developing programs from Z specifications.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.sx.ac.uk