Revising Z: part I - logic and semantics

Abstract

This is the first of two related papers. We introduce a simple specification logic ZC comprising a logic and a semantics (in ZF set theory) within which the logic is sound. 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 a basic schema calculus.