Abstract
Z is gaining ground in the software development community as a specification language, but there is at present no standard way of relating a Z specification to program code. Hoare logics have been around for about 20 years. They are well understood and widely taught as a method of proving that a program meets its specification. In this paper I look at how a software development might use both techniques and both notations to provide a path from a high- level Z specification to program code. Rules and conventions for combining the two notations are given and their use is illustrated by two case studies.
This is a preview of subscription content, log in via an institution to check access.
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
Alagic, S., and M. A. Arbib, (1978), The Design of Well-Structured and Correct Programs, Berlin, Springer-Verlag.
Baber, R.L., (1987), The Spine of Software: Designing Provably Correct Software: Theory and Practice, or a Mathematical Introduction to the Semantics of Computer Programs, Chichester, Wiley.
Backhouse, R.C., (1986), Program Construction and Verification, Hemel Hempstead, Prentice Hall.
Cousot, P., (1990), “Methods and Logics for Proving Programs”, in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, vol. B, Formal Models and Semantics, Amsterdam, Elsevier, 1990, pp. 841–993.
Diller, A., (1990), Z: An Introduction to Formal Methods, Chichester, Wiley.
Diller, A., (1991), Relating Z Specifications and Programs Through Hoare Logics, Research Report CSR-91-3, School of Computer Science, University of Birmingham.
Dromey, R.G., (1989), Program Derivation: The Development of Programs from Specifications, Wokingham, Addison-Wesley.
Gilmore, S., (1991), Correctness-oriented Approaches to Software Development, Internal Report CST-76-91, Department of Computer Science, University of Edinburgh. (Also Report ECS-LFCS-91-147, Laboratory for Foundations of Computer Science, University of Edinburgh.)
Gordon, M.J.C., (1988), Programming Language Theory and its Implementation: Applicative and Imperative Paradigms, Hemel Hempstead, Prentice Hall.
Gries, D., (1981), The Science of Programming, Berlin, Springer-Verlag.
Gumb, R.D., (1989), Programming Logics: An Introduction to Verification and Semantics, Chichester, Wiley.
Hayes, I., (ed.), (1987), Specification Case Studies, Hemel Hempstead, Prentice Hall.
Hoare, C.A.R., (1969), “An Axiomatic Basis for Computer Programming”, Communications of the ACM, vol. 12, pp. 576–580 and 583.
Hoare, C.A.R., (1971), “Procedures and Parameters: An Axiomatic Approach”, in E. Engeler (ed.), Symposium on Semantics of Algorithmic Languages, Berlin, Springer-Verlag, 1971, pp. 102–116.
Ince, D.C., (1988), An Introduction to Discrete Mathematics and Formal System Specification, Oxford, Oxford University Press.
Jones, C.B., (1986), Systematic Software Development Using VDM, Hemel Hempstead, Prentice Hall.
Kaldewaij, A., (1990), Programming: The Derivation of Algorithms, Hemel Hempstead, Prentice Hall.
King, S., (1990), Z and the Refinement Calculus, Technical Monograph PRG-79, Oxford University Computing Laboratory.
Lightfoot, D., (1991), Formal Specification Using Z, Basingstoke, Macmillan.
Morgan, C., (1990), Programming from Specifications, Hemel Hempstead, Prentice Hall.
Morgan, C., K. Robinson and P. Gardiner, (1988), On the Refinement Calculus, Technical Monograph PRG-70, Oxford University Computing Laboratory.
Nielson, H.R., and F. Nielson, (1992), Semantics with Applications: A Formal Introduction, Chichester, Wiley.
Norcliffe, A., and G. Slater, (1991), Mathematics of Software Construction, Chichester, Ellis Horwood.
Potter, B., J. Sinclair and D. Till, (1991), An Introduction to Formal Specification and Z, Hemel Hempstead, Prentice Hall.
Spivey, J.M., (1988), Understanding Z: A Specification Language and its Formal Semantics, Cambridge, Cambridge University Press.
Spivey, J.M., (1989), The Z Notation: A Reference Manual, Hemel Hempstead, Prentice Hall.
Woodcock, J.C.P., and M. Loomes, (1988), Software Engineering Mathematics: Formal Methods Demystified, London, Pitnam.
Wordsworth, J.B., (1988), Specification and Refinement using Z and the Guarded Command Language: A Compendium, IBM United Kingdom Laboratories Ltd., Hursley.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 British Computer Society
About this paper
Cite this paper
Diller, A. (1992). Z and Hoare Logics. 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_3
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3203-5_3
Publisher Name: Springer, London
Print ISBN: 978-3-540-19780-5
Online ISBN: 978-1-4471-3203-5
eBook Packages: Springer Book Archive