Abstract
This paper describes a formal object-oriented specification language, Z++, and identifies proof rules and associated specification structuring and development styles for the facilitation of validation and verification of implementations against specifications in this language. We give inference rules for showing that certain forms of inheritance lead to refinement, and for showing that refinements are preserved by constructs such as promotion of an operation from a supplier class to a client class. Extension of these rules to other languages is also discussed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A. Alencar, J. Goguen: OOZE: An Object-Oriented Z Environment. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag LNCS, Vol 512, 1991.
R.J.R Back, A Calculus of Refinements for Program Derivation, Acta Informatica 25, 593–624 (1988).
J.L. Bell, Boolean-valued models and independence proofs in set theory, Oxford Logic Guides 12, Clarendon Press, Oxford 1977.
P. Breuer, K. Lano, From Code to Z Specifications. In: J. Nicholls (ed.): Z User Meeting 1989, in Springer-Verlag Workshops in Computer Science, 1990.
P. Breuer, K. Lano, Creating Specifications from Code: Reverse-Engineering Techniques, Journal of Software Maintenance, September 1991.
E. Cusack, Object-Oriented Modelling in Z. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag Lecture Notes in Computer Science, Vol 512, 1991.
A. Diller, Z: An Introduction to Formal Methods, Wiley, 1991.
D. Duke, R. Duke, P. King, G. A. Rose, G. Smith, Object-Z: An Object-Oriented Extension to Z, technical report 91-1, Software Verification Research Centre, The University of Queensland.
R. Duke, P. King, G. Smith, Formalising Behavioural Compatibility for Reactive Object-Oriented Systems. In: P. America (ed.): ECOOP '91 Proceedings, Springer-Verlag Lecture Notes in Computer Science, Vol. 512, 1991.
H. Haughton, K. Lano, An Algebraic Semantics for the Specification Language Z ++, AMAST '91 Conference, Iowa. To appear in Springer-Verlag Workshops in Computer Science.
H. Haughton, K. Lano, Using Formal Methods in Artificial Intelligence, IJCAI '91 Workshop on Software Engineering for Knowledge-Based Systems, Sydney, August 1991.
C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall 1985.
K. Lano, H. Haughton, P. Breuer, Reverse-Engineering of Library Case Study, REDO Document 2487-TN-PRG-1064, April 1991.
K. Lano, H. Haughton, Axioms for Object-Oriented Extensions to Z, ZOOM Workshop, Oxford University Programming Research Group, 1991.
K. Lano, Z ++, an Object-Oriented Extension to Z. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 151–172, 1991.
K. Lano, The Design of the Verification Toolset, REDO Project Document 2487-TN-PRG-1068, Oxford University Programming Research Group, 1991.
K. Lano, Integrating Development and Maintenance in an Object-Oriented Environment, REDO Document 2487-TN-PRG-1050, Oxford University Programming Research Group, 1991.
S. Leonard, J. Pardoe, S. Wade, Software Maintenance — Cinderella is Still not Getting to the Ball. In: BCS/IEE Conference on Software Engineering 1988, IEE London, 104–106, 1988.
P. Lupton, Promoting Forward Simulation. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.
J. A. McDermid, P. J. Whysall, Object Oriented Specification and Refinement. In: Proceedings of the 4th Refinement Workshop, Cambridge, Springer-Verlag Workshops in Computing, 1991.
S. Meira, A.L.C. Cavalcanti, Modular Object-oriented Z Specifications. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.
B. Meyer, Tools for the New Culture: Lessons from the Design of the Eiffel Libraries, Communications of the ACM, September 1990, Vol 33, No. 9.
D. Monk, Mathematical Logic, North Holland, 1979.
C. Morgan, K. Robinson, P. Gardiner, On The Refinement Calculus, PRG Monograph PRG-70, 1988, Oxford University Programming Research Group.
J. M. Morris, A theoretical basis for stepwise refinement and the programming calculus, Science of Computer Programming, 9(3), 298–306, December 1987.
D. Neilson, Machine Support for Z: the zedB tool, Z User Meeting 1990. In: J. Nicholls (ed.): Z User Workshop, Oxford 1990, Springer-Verlag Workshops in Computing, 1991.
C. Stanley-Smith, A. Cahill, UNIFORM: A Language Geared To System Description and Transformation, University of Limerick, 1990.
I. SØrensen, The B Method, VDM '91, Noodwijkerhout, Netherlands, 1991.
M. Spivey, Understanding Z, CUP, Cambridge, 1988.
M. Spivey, The Z Notation: A Reference Manual, Prentice Hall 1989.
A. Wills, Capsules and Types in Fresco. In: P. America (ed.): ECOOP '91 Proceedings, Springer Verlag Lecture Notes in Computer Science, Vol 512, 1991.
J. Woodcock, S. Brien, W: A Logic for Z, Oxford University Programming Research Group, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lano, K., Haughton, H. (1992). Reasoning and refinement in object-oriented specification languages. In: Madsen, O.L. (eds) ECOOP ’92 European Conference on Object-Oriented Programming. ECOOP 1992. Lecture Notes in Computer Science, vol 615. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053031
Download citation
DOI: https://doi.org/10.1007/BFb0053031
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55668-8
Online ISBN: 978-3-540-47268-1
eBook Packages: Springer Book Archive