Revising Z: semantics and logic

Abstract

We introduce a simple specification logic Zc comprising a logic and semantics (in ZF set theory). We then provide an interpretation for (a rational reconstruction of) the specification language Z within Zc. As a result we obtain a sound logic for Z, including the schema calculus. A consequence of our formalisation is a critique of a number of concepts used in Z. We demonstrate that the complications and confusions which these concepts introduce can be avoided without compromising expressibility.