W Reconstructed
Jon Hall and Andrew Martin
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.
Address
Berlin Heidelberg
Annote
10th International Conference of Z Users‚ University of Reading‚ April 1997‚ Proceedings
Book Title
ZUM'97: The Z Formal Specification Notation‚ 10th International Conference of Z Users‚ Reading‚ UK‚ April 1997‚ Proceedings
Editor
Jonathan P. Bowen and Michael G Hinchey and David Till
ISBN
3−540−62717−0
Month
apr
Publisher
Springer−Verlag
Series
Lecture Notes in Computer Science
Volume
1212
Year
1997