Abstract
As part of a general effort to provide a new basis for software development through reuse of “Trusted Components”, we outline a scheme for proving that classes equipped with contracts in the Eiffel style meet these contracts. The approach takes advantage of the inheritance structure to separate proof obligations between deferred (abstract) classes, to be validated against a model, and their effective implementations, which then must only be proved against the contracts of the deferred ancestors. The testbed for this study is the EiffelBase library of fundamental data structures and algorithms, whose classes include extensive contracts.
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.
References
Jean-Raymond Abrial: The B Book, Cambridge University Press, 2002
Felix Bachmann, Len Bass, Charles Buhman, Santiago Comella-Dorda, Fred Long, John Robert, Robert Seacord, Kurt Wallnau: Technical Concepts of Component-Based Software Engineering, Software Engineering Institute CMU/SEI-2000-TR-008, 2000, available at http://www.sei.cmu.edu/publications/documents/00.reports/00tr008.html.
Bertrand Meyer, Reusability: the Case for Object-Oriented Design, in IEEE Software, vol. 4 no. 2, March 1987, pages 50–62. Also in: Selected Reprints in Software, ed. M. Zelkowitz, IEEE Press, 1987; Software Reusability, ed. T. Biggerstaff, Addison-Wesley, 1988; Object-Oriented Computing, IEEE Press, 1988.
Bertrand Meyer: Applying “Design by Contract”, in IEEE Computer, 2510, October 1992, pages 40. Also in Object-Oriented Systems and Applications, ed. David Rine, IEEE Computer Press, 1994.
Bertrand Meyer: Eiffel: The Language, Prentice Hall, second printing, 1991.
Bertrand Meyer: Reusable Software: The Base Object-Oriented Libraries, Prentice Hall, 1994.
Bertrand Meyer: Object-Oriented Software Construction, second edition, Prentice Hall, 1997.
Bertrand Meyer, Christine Mingins and Heinz Schmidt: Providing Trusted Components to the Industry, in IEEE Computer, vol. 31 no. 5, May 1998, pages 104–105.
Bertrand Meyer: Contracts for Components, in Software Development, vol. 8 no. 7, July 2000, pages 51–53.
Bertrand Meyer: Towards a Component Quality Model, working paper at http://www.inf.ethz.ch/~meyer.
Bertrand Meyer: Proving Program Pointer Properties, working paper at http://www.inf.ethz.ch/~meyer.
Robert F. Stärk, Egon Borger and Joachim Schmid: Java and the Java Virtual Machine: Definition, Verification, Validation, Springer-Verlag, 2001.
Clemens Szyperski: Component Software: Beyond Object Oriented Programming. Addison-Wesley, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, B. (2003). A Framework for Proving Contract-Equipped Classes. In: Börger, E., Gargantini, A., Riccobene, E. (eds) Abstract State Machines 2003. ASM 2003. Lecture Notes in Computer Science, vol 2589. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36498-6_6
Download citation
DOI: https://doi.org/10.1007/3-540-36498-6_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00624-4
Online ISBN: 978-3-540-36498-6
eBook Packages: Springer Book Archive