| W Reconstructed (2007) | |||||||||||||||
Abstract | |||||||||||||||
| An early version of the Z Standard included the deductive system W for reasoning about Z specifications. Later versions contain a different deductive system. In this paper we sketch a proof that 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 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. 1 Introduction An important part of the Z Standardization activity has been the definition of a logical deductive system for Z. Whilst some have sought to provide support for reasoning about Z specifications by embedding the language in an existing well-understood framework (HOL, Eves, PVS, Isabelle, for example; [BG94,Jon92,Saa92,KSW96,ES94]), other research has attempted to provide support for reasoning within Z, making use of Z's type ... | |||||||||||||||
Publication details | |||||||||||||||
| |||||||||||||||