Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 8, Issue 1: February 1998.

Constructive Z

S-H Mirian-Hosseinabadi1 and R Turner2

1Department of Computer Science, University of Essex, Wivenhoe Park, Colchester, C04 3SQ, UK. E-mail: seymh@essexac.uk, 2Department of Computer Science, University of Essex, Wivenhoe Park, Colchester, C04 3SQ, UK. E-mail: tumr@essexac.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.

Pages 49-70


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_01/080049.sgm.abs.html
Last modification: 1 June 1998.
Copyright© Oxford University Press, 1998.