A logic for the schema calculus

Abstract

In this paper we introduce and investigate a logic for the schema calculus of Z. The schema calculus is arguably the reason for Z’s popularity but so far no true calculus (a sound system of rules for reasoning about schema expressions) has been given. Presentations thus far have either failed to provide a calculus (e.g. the draft standard [3]) or have fallen back on informal descriptions at a syntactic level (most text books e.g. [7]). Once the calculus is established we introduce a derived equational logic which enables us to formalise properly the informal notations of schema expression equality to be found in the literature.