A Framework for Proving Contract-Equipped Classes

r in: Abstract State Machines 2003 — Advances in Theory and Applications, Proc. 10th International Workshop, Taormina, Italy, March 3-7, 2003, eds. Egon Boerger, Angelo Gargantini, Elvinia Riccobene, Springer-Verlag 2003. A framework for proving contract-equipped classes Bertrand Meyer ETH Zürich, Chair of Software Engineering (also Eiffel Software, Santa Barbara) se.inf.ethz.ch 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 ons 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 incl...

• Type: Conference
• Year: 2003
• Where: ASM
• Authors: Bertrand Meyer
• Keywords: ASM 2003, General Effort, Microbiology, Reusable Components, Reuse