Revising Z: semantics and logic
Martin C. Henson, Steve Reeves · 1998
. 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. Keywords: Specification language Z ; Logics and semantics of specification languages 1. Introduction 1.1. Background The specification language Z has been in existence, and has been very widely used, for more than a decade. In view of this, it is perhaps somewhat surprising to discover that there exists no definitive account of either its proof theory or semantics. The variety of distinct interpretations one can find in the wealth of textbooks (e.g. [PST96], [BJ95], [Bow96], [Dil90], [...