Details of Grant 

EPSRC Reference:	GR/J46630/01
Title:	MODELS, ALGEBRA AND MECHANICAL SUPPORT IN Z
Principal Investigator:	Hoare, Professor Sir C
Other Investigators:	Woodcock, Professor JCP
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Oxford
Scheme:	Standard Research (Pre-FEC)
Starts:	01 January 1994	Ends:	31 December 1995	Value (£):	83,309
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Related Grants:
Panel History:
Summary on Grant Application Form
To combine the advantages of model based and algebraic techniques in specification1. Completion of the definition of the model and axiomatisation of Z2. Derivation of general and application-specific laws with machine support3. Illustrating the use on case studies of embedded real-time systemsProgress:1. Work on the model and axiomatisation of Z was essentially complete before the departure of S. M. Brien in October. It will be published as his D. Phil. thesis. It has already proved its value to the Z Standards Review Committee, particularly in guiding its decisions on the question of undefinedness of functions. 2. A. P. Martin took over from S. M. Brien when he left to pursue another career. His work to date has involved familiarising himself with the work of Brien, and with possible technologies for the achievement of objective (2) above. 20BJ, which was proposed for this task, is no longer supported. Instead, we propose a proof tool for Z written a functional language. Martin has invested some effort in exploring how the algebra of monads can be used in this setting, to implement proof tactics explored in his D.Phil. thesis. It is planned that this proof tool should be available, at least in prototype form, for the 1995 Z User Meeting in September. Martin has also joined the Z Standards Committee, and will edit the chapter of the standard which deals with deductive systems for Z. The laws presented in that chapter may, if time permits, be proved sound with respect to Briens work, and will form the basis for the proof tool described above.3. Work on case studies is pursued in a collaborative project.
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.ox.ac.uk