# 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