We report on an analysis of the inheritance relationships in the Eiffel Base Libraries, a library of container data structures. If inheritance is behaviorally conforming, then polymorphism can be used safely, and the inheritance hierarchy can be considered part of the interface of the library to its clients. We describe a theory of object-oriented specification in higher-order logic that we used to specify part of the Eiffel Base Libraries. With the theorem prover Isabelle/HOL, we mechanically prove conformance relationships between those specifications. This work allows us to draw conclusions about the design of the Eiffel Base Libraries, and about the feasibility of using an interactive theorem prover to apply a strictly formal theory to the specification of a commercial product. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Helke, S., & Santen, T. (2001). Mechanized analysis of behavioral conformance in the Eiffel Base Libraries. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2021 LNCS, pp. 20–42). Springer Verlag. https://doi.org/10.1007/3-540-45251-6_3
Mendeley helps you to discover research relevant for your work.