Abstract
Inconsistent specifications may give rise to false conclusions in reasoning, thus destroying the point of having a specification. This report is concerned with inconsistent specifications which may arise when using the formal specification language Z. In particular, the report is concerned with the inconsistencies that can arise when using recursive free types, and recursive functions defined over recursive free types. The intended audience of the report consists of Z practitioners who wish to avoid writing meaningless specifications.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
The HOL System (Description), SRI International, Cambridge Research Centre, December 1989.
T. F. Melham, “Automating Recursive Type Definitions in Higher Order Logic”, in Current Trends in Hardware Verification and Automated Theorem Proving, edited by G. Birtwistle and P.A. Subrahmanyam (Springer-Verlag, 1989), pp. 341–386.
J. M. Spivey, The Z Notation, Prentice Hall International, 1989.
J. M. Spivey, Understanding Z, Cambridge University Press, 1988.
J.M. Spivey, “Free Type Definitions”, in Proceedings of the Third Annual Z Users Meeting, Oxford University Computing Laboratory, Programming Research group, December 1988.
R. D. Arthan, On Free Type Definitions in Z, Issue 1.7, ICL Defence Systems, ref DS/FMU/IED/WRK/016, April 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1991 British Crown Copyright
About this paper
Cite this paper
Smith, A. (1991). On Recursive Free Types in Z. In: Nicholls, J.E. (eds) Z User Workshop, York 1991. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3203-5_1
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3203-5_1
Publisher Name: Springer, London
Print ISBN: 978-3-540-19780-5
Online ISBN: 978-1-4471-3203-5
eBook Packages: Springer Book Archive