| EPSRC Reference: |
GR/L57913/01 |
| Title: |
IMPLEMENTING CONSTRUCTIVE Z |
| Principal Investigator: |
Turner, Professor R |
| Other Investigators: |
|
| 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 |