Jon Hall and Andrew Martin
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.
10th International Conference of Z Users‚ University of Reading‚ April 1997‚ Proceedings
ZUM'97: The Z Formal Specification Notation‚ 10th International Conference of Z Users‚ Reading‚ UK‚ April 1997‚ Proceedings
Jonathan P. Bowen and Michael G Hinchey and David Till
Lecture Notes in Computer Science