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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Jonathan P. Bowen and Mike J. C. Gordon. Z and HOL. In J. P. Bowen and J. A. Hall, editors, Z User Workshop, Cambridge 1994, Workshops in Computing, pages 141–167. Springer-Verlag, 1994.
Jonathan P. Bowen and Michael G. Hinchey, editors. ZUM'95: The Z Formal Specification Notation, volume 967 of LNCS. Springer-Verlag, 1995.
S. M. Brien, J. E. Nicholls, et al. Z base standard. ZIP Project Technical Report ZIP/PRG/92/121, SRC Document: 132, Version 1.0, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, November 1992.
Stephen M. Brien. A Model and Logic for Generically Typed Set Theory (Z). D.Phil. thesis, University of Oxford, 1995. New version expected 1996.
Marcin Engel and Jens Ulrik Skakkeebæk. Applying PVS to Z. ProCoS II Technical Report IT/DTU ME 3/1, Department of Computer Science, Technical University of Denmark, December 1994.
W. T. Harwood. Proof rules for Balzac. Technical Report WTH/P7/001, Imperial Software Technology, Cambridge, UK, 1991.
R. B. Jones. ICL ProofPower. BCS FACS FACTS, Series III, 1(1):10–13, Winter 1992.
Ina Kraan and Peter Baumann. Implementing Z in Isabelle. In Bowen and Hinchey [BH95], pages 355–373.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In 1996 International Conference on Theorem Proving in Higher Order Logic. Springer-Verlag, 1996.
Andrew Martin. Encoding W: A Logic for Z in 2OBJ. In J. C. P. Woodcock and P. G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, volume 670 of Lecture Notes in Computer Science, pages 462–481. Springer-Verlag, 1993.
A. P. Martin, P. H. B. Gardiner, and J. C. P. Woodcock. A tactic calculus. Formal Aspects of Computing, 8(4):479–489. Springer-Verlag, 1996.
John Nicholls, editor. Z Notation. Z Standards Panel, ISO Panel JTC1/SC22/ WG19 (Rapporteur Group for Z), 1995. Version 1.2, ISO Committee Draft.
M. Saaltink. Z and Eves. In J. E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, pages 223–242. Springer-Verlag, 1992.
Graeme Smith. Extending W for Object-Z. In Bowen and Hinchey [BH95], pages 276–295.
I. Toyn and J.G. Hall. Proving Conjectures using Cadiℤ. Cadiℤ documentation (to appear as a York University Technical Report).
I. Toyn and J.A. McDermid. Cadiℤ: An architecture for Z tools and its implementation. Software—Practice and Experience, 25(3):305–330, 1991.
J. C. P. Woodcock and S. M. Brien. W: A Logic for Z. In Proceedings 6th Z User Meeting. Springer-Verlag, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hall, J., Martin, A. (1997). W Reconstructed. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds) ZUM '97: The Z Formal Specification Notation. ZUM 1997. Lecture Notes in Computer Science, vol 1212. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027287
Download citation
DOI: https://doi.org/10.1007/BFb0027287
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62717-3
Online ISBN: 978-3-540-68490-9
eBook Packages: Springer Book Archive