Investigating Z
Martin C. Henson · Journal of Logic and Computation · 2000
In this paper we introduce and investigate an improved kernel logic ZC for the specification language Z. Unlike the standard accounts, this logic is consistent and is easily shown to be sound. We show how a complete schema calculus can be derived within this logic and in doing so we reveal a high degree of logical organisation 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. Keywords: Specification language Z; Logic and semantics of specification languages. 1 Introduction In this paper we introduce and investigate an improved kernel logic ZC for the specification language Z, a logic in which, in particular, we can derive a schema calculus: a logic for the entire range of schema expressions permit...