Investigating Z

Abstract

In this paper we introduce and investigate an improved kernel logic Zc for the specification language Z. Unlike standard accounts, this logic is consistent and is easily shown to be sound. We show how a complete shema calculus can be derived within this logic and in doing so we reveal a high degree of logical organization within the language. Finally, our approach eschews all non-standard concepts introduced in the standard approach, notably object level notions of substitution and entities which share properties both of constants and variables. We show, in addition, that these unusual notions are derivable in Zc and are, therefore, unnecessary innovations.