© 1998 by Oxford University Press
Original Articles |
Constructive Z
Department of Computer Science, University of Essex Wivenhoe Park, Colchester, CO4 3SQ, UK E-mail: seymh{at}essex.ac.uk
Department of Computer Science, University of Essex Wivenhoe Park, Colchester, CO4 3SQ, UK E-mail: turnr{at}essex.ac.uk
An approach to Z-style program specification is developed based upon a constructive version of Zermelo-Fraenkel set theory without replacement. The idea of obligation schema, an extension of Z-schema, is introduced, and an implementation of this notion presented which facilitates the abstraction of programs.
Keywords: Z; specification; type-theory; constructive; schema