Abstract
In this paper we present a method for using generic components in formal specifications. This approach results in a flexible generic system description that separates the concerns of structure and data types. The generic specification can be extended and modified in a natural manner, to track requirements as they inevitably evolve during the development process. In addition, the specification can readily be specialised to use more concrete data types without the need for a formal refinement, using explicit generic instantiation. Such generic instantiation also allows operation preconditions to be strengthened; this is not allowed by classic refinement, but it permits a separation of concerns by allowing preconditions relevant to specialised data types to be added only when they become relevant.
Acknowledgements
The work described in this paper derives in part from work undertaken during and as a result of the SAZ project, 1990-94, EPSRC grants (GR/J81655) and (GR/F98642). We would like to thank Sam Valentine and Ian Toyn for helpful discussions.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 2nd Edition, 1992.
R. Barden, S. Stepney, D. Cooper. Z In Practice. Prentice Hall, 1994.
B. Potter, J. Sinclair, and D. Till. An Introduction to Formal Specification and. Prentice Hall, 2nd Edition, 1996.
J. C. P. Woodcock and J. Davies. Using Z: Specificaion, Refinent, and Proof Prentice Hall, 1996.
M. d’Inverno and M. Priestley. Structuring Specification to Build a Unifying Framework for Hypertext Systems. ZUM’95: The Z Formal Specification Notation; Proceedings of Ninth International Conference of Z Users, Limerick, Ireland, September 1995, pp83–102. LNCS 967. Springer Verlag, 1995.
L. T. Semmens, R. B. France, and T. W. G. Docker. Integrated Structured Analysis and Formal Specification Techniques The Computer Journal, vol 35, no 6, 1992.
R. B. France and M. M. Larrondo-Petrie. A Two-Dimensional View of Integrated Formal and Informal Specification Techniques. ZUM’95: The Z Formal Specification Notation; Proceedings of Ninth International Conference of Z Users, Limerick, Ireland, September 1995, pp434–448. LNCS 967. Springer Verlag, 1995.
F. A. C. Polack, M. Whiston, and P. Hitchcock. Structured Analysis A Draft Method for Writing Z Specifications. Proceedings of Sixth Annual Z User Meeting, York, Dec 1991. Springer Verlag, 1992.
F. Polack, M. Whiston, and K.C. Mander. The SAZ Project: Integrating SSADM and Z. Proceedings, FME’93: Industrial Strength Formal Methods, Odense, Denmark, April 1993. LNCS 670. Springer Verlag, 1993
F. Polack, M. Whiston, and K. C. Mander. The SAZ Method Version 1.1. York, YCS 207, Jan 1994.
I. Hayes. Specification Case Studies. Prentice Hall, 2nd Edition, 1992.
S. Stepney. A Tale of Two Proofs. Proceedings, 3rd Northern Formal Methods Workshop, Ilkley, Sept 1998. BCS-FACS, 1998.
S. Stepney, D. Cooper, and J. C. P. Woodcock. More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. ZUM’98: 11th international conference of Z Users, Berlin. LNCS 1493. Springer Verlag, 1998.
E. Boiten and J. Derrick. IO-Refinement in Z. Proceedings, 3rd Northern Formal Methods Workshop, Ilkley, Sept 1998. BCS-FACS, 1998.
R. Banach and M. Poppleton. Retrenchment: An Engineering Variation on Refinement. Proceedings, B98, Montpellier, France. LNCS 1393. Springer Verlag, 1998.
I. Hayes. Specification Models. Z Twenty Years On: What Is Its Future?, Nantes, France, October 1995. 1995.
I. J. Hayes and M. Utting. Coercing real-time re nement: A transmitter Northern Formal Methods Workshop, Ilkley, UK, September 1995. 1995.
CCTA. SSADM Version 4 Reference Manual. NCC Blackwell Ltd, 1990.
H. E. D. Parker, F. Polack, and K. C. Mander The Industrial Trial of SAZ: Reflections on the Use of an Integrated Specification Method. Z Twenty Years On: What Is Its Future?, Nantes, France, October 1995.
F. A. C. Polack and K. C. Mander. Software Quality Assurance Using the SAZ Method. Proceedings of Eighth Annual Z User Meeting, Cambridge, June 1994. Springer Verlag, 1994.
L. Semmens and P. Allen. Using Yourdon and Z: an Approach to Formal Specification. Proceedings of Fifth Annual Z User Meeting, Oxford, Dec 1990. Springer-Verlag, 1991.
D. Redmond-Pyle and M. Josephs. Enriching a Structured Method with Z. Work-shop on Methods Integration, 26 September 1991, Leeds, (unpublished)
C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Polack, F., Stepney, S. (1999). Systems development using Z generics. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_6
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive