Abstract
Object-oriented languages provide advantages such as reuse and modularity, but they also raise new challenges for program verification. Program logics have been developed for languages such as C# and Java. However, these logics do not cover the specifics of the Eiffel language. This paper presents a program logic for Eiffel that handles exceptions, once routines, and multiple inheritance. The logic is proven sound and complete w.r.t. an operational semantics. Lessons on language design learned from the experience are discussed.
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
Banerjee, A., Naumann, J.D.A., Rosenberg, S.: Regional Logic for Local Reasoning about Global Invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 387–411. Springer, Heidelberg (2008)
Bannwart, F.Y., Müller, P.: A Logic for Bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE). ENTCS, vol. 141(1), pp. 255–273. Elsevier, Amsterdam (2005)
Distefano, D., Parkinson, M.J.: jStar: Towards Practical Verification for Java. In: OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN conference on Object oriented programming systems languages and applications, pp. 213–226 (2008)
Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)
Kassios, I.T.: Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)
Leino, K.R.M., Müller, P.: Modular Verification of Static Class Invariants. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 26–42. Springer, Heidelberg (2005)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)
Meyer, B. (ed.): ISO/ECMA Eiffel standard (Standard ECMA-367: Eiffel: Analysis, Design and Programming Language) (June 2006), http://www.ecma-international.org/publications/standards/Ecma-367.htm
MOBIUS Consortium. Deliverable 3.1: Byte code level specification language and program logic (2006), http://mobius.inria.fr
Müller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp. 39–46 (2007)
Nordio, M., Calcagno, C., Müller, P., Meyer, B.: Soundness and Completeness of a Program Logic for Eiffel. Technical Report 617, ETH Zurich (2009)
Nordio, M., Müller, P., Meyer, B.: Proof-Transforming Compilation of Eiffel Programs. In: Paige, R., Meyer, B. (eds.) TOOLS-EUROPE 2008. LNBIP, vol. 11. Springer, Heidelberg (2008)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268–280 (2004)
Parkinson, M.J., Bierman, G.: Separation logic and abstraction. In: POPL 2005, vol. 40, pp. 247–258. ACM Press, New York (2005)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL 2008, pp. 75–86. ACM Press, New York (2008)
Pavlova, M.: Java Bytecode verification and its applications. PhD thesis, University of Nice Sophia-Antipolis (2007)
Poetzsch-Heffter, A., Müller, P.: Logical Foundations for Typed Object-Oriented Languages. In: Gries, D., De Roever, W. (eds.) Programming Concepts and Methods (PROCOMET), pp. 404–423 (1998)
Poetzsch-Heffter, A., Müller, P.O.: A Programming Logic for Sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)
Poetzsch-Heffter, A., Rauch, N.: Soundness and Relative Completeness of a Programming Logic for a Sequential Java Subset. Technical report, Technische Universität Kaiserlautern (2004)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
Schoeller, B.: Making classes provable through contracts, models and frames. PhD thesis, ETH Zurich (2007)
Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. In: Formal Techniques for Java-like Programs (2008)
von Oheimb, D.: Analyzing Java in Isabelle/HOL - Formalization, Type Safety and Hoare Logic. PhD thesis, Universität München (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nordio, M., Calcagno, C., Müller, P., Meyer, B. (2009). A Sound and Complete Program Logic for Eiffel. In: Oriol, M., Meyer, B. (eds) Objects, Components, Models and Patterns. TOOLS EUROPE 2009. Lecture Notes in Business Information Processing, vol 33. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02571-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-02571-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02570-9
Online ISBN: 978-3-642-02571-6
eBook Packages: Computer ScienceComputer Science (R0)