New foundations for Z
Martin C. Henson, Steve Reeves · 1998
. We provide a constructive and intensional interpretation for the specification language Z in a theory of operations and kinds T . The motivation is to facilitate the development of an integrated approach to program construction. We illustrate the new foundations for Z with examples. 1 Introduction The standard account of the foundations of the specification language Z is given in classical, extensional set theory. In this paper we explore the consequences of an alternative, based on a constructive, intensional set theory. We are not suggesting that the standard model is in any way intrinsically inadequate; rather that there may be an alternative with a different set of practical consquences for specification and, in particular, for program development. There is, of course, also mathematical interest involved in exploring this different choice of foundation. 2 Foundations of Z : some suggestions 2.1 Extensional or intensional sets? The standard interpretation of functions in Z is t...