Department of Computer Science  New Foundations for Z 
  
 
 

 
 

Contents

Introduction

This research is a joint project which is currently under investigation by: 

The standard account of the foundations of the specification language Z is given in classical, extensional set theory.  We aim explore the consequences of an alternative, based on a  constructive, intensional set theory. Our motivation is the integration of specification with program development: a goal which has has proved elusive in the standard model. 

This work has been fundedby the Royal Society of Great Britain,the University of Waikato and theCentre for Discrete Mathematics andTheoretical Computer Science, New Zealand.  

Research Plan

The basic plan of this research: 

  • Settle on foundations for Z as it currently standsÑthis has been done by introducing an intermediate, kernel language ZC which is expressive enough to support Z in full but which is simple enough to provide clear semantics via classical ZF set-theory and classical logic.
  • Develop a satisfactory logic for the Schema Calculus.
  • Replace ZF and classical logic with a constructive and intensional logic and set theory based on systems similar to those developed by Beeson and Feferman.
  • Develop programs within Z (via the usual constructive interpretation of, roughly, programs as proofs) and differentiate between different implementations (via the intensional nature of the set theory).

Examples

The examples we give here are rather trivial. They nonetheless illustrate the strategy we are adopting and, hopefully, indicate in outline how we proceed in more ambitious cases. 

In our constructive and intensional Z operation schema are distinguished from state schema and to each operation schema we associate a Program Construction Obligation:  

The PCO can then be proved in the logic for Z:    It is then possible to obtain the computational content of this proof by injecting the derivation into a term-assignment formulation of the foundational system:  

We have shown the proof explicitly in the underlying foundational system in order to illustrate how the process works. Because, however, the proof which the program developer undertakes is in the higher level logic for Z, we may make use of higher level programming constructs. In particular, using simple techniques from denotational semantics, the program derivation above has computational content: z := z + 1. As a consequence of the mathematics we may also conclude that: z := z + 1 e Inc. 

But perhaps the most interesting and encouraging aspects of this approach is the use we may make of the schema calculus for not only structuring specifications but also structuring program constructions:  The rule we have employed here is the rule for introducing implementations of schema expressions involving composition of schemas:  

An alternative is to derive a program in terms of sequencing:  One of a number of interesting ways of using conjunction in the operation schema calculus is for decomposing a specification into looser components: 
  

Finally, we can use disjunction of operation schema to introduce alternation. This, unsurprisingly, involves conditionals in the derived program. The example which follows is rather artificial but illustrates the technique:  

Here is a program derivation for Op0:  
The programs which we can obtain from this, and the other component schema are:  Then:  

Publications

The following are all joint publications by Martin Henson and Steve Reeves: 


 

Related Work

Another project based at Essex is also investigating ways of providing badly needed support tools to aid the construction of derivations in this constructive, intensional version of Z. 

Our work should be seen as complimentary to the effort via the ISO panel on standardizing Z (on which Steve Reeves is the New Zealand representative) which is seeking to put Z, approximately as presented in many current textbooks, on a standardized and sure footing. 

There are links to other people working in formal methods in New Zealand on the Formal Program Development Colloquium web page. 

The focal point for much related work can be found in Jonathan Bowen's  Virtual library of formal methods 

Other Work

Thomas Santen's site on HOL-Z 
 


Top of page 

Web-administrator, Department of Computer Science, University of Waikato, Hamilton, New Zealand