W Reconstructed

Abstract

An early version of the Z Standard included the deductive system \cal W for reasoning about Z specifications. Later versions contain a different deductive system. In this paper we sketch a proof that \cal W is relatively sound with respect to this new deductive system. We do this by demonstrating a semantic basis for a correspondence between the two systems, then showing that each of the inference rules of \cal W can be simulated as derived rules in the new system. These new rules are presented as tactics over the the inference rules of the new deductive system.