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.
Details
| 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 |
Links
Related pages
|
People |