Abstract
Abadi-Leino Logic is a Hoare-calculus style logic for a simple imperative and object-based language where every object comes with its own method suite. Consequently, methods need to reside in the store (”higher-order store”). We present a new soundness proof for this logic using a denotational semantics where object specifications are recursive predicates on the domain of objects. Our semantics reveals which of the limitations of Abadi and Leino’s logic are deliberate design decisions and which follow from the use of higher-order store. We discuss the implications for the development of other, more expressive, program logics.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, New York (1996)
Abadi, M., Leino, K.R.M.: A logic of object-oriented programs. In: Dershowitz, N. (ed.) Verification: Theory and Practice, pp. 11–41. Springer, Heidelberg (2004)
Amadio, R.M., Cardelli, L.: Subtyping recursive types. ACM Transactions on Programming Languages and Systems 15(4), 575–631 (1993)
Apt, K.R.: Ten years of Hoare’s logic: A survey — part I. ACM Transactions on Programming Languages and Systems 3(4), 431–483 (1981)
de Boer, F.S.: A WP-calculus for OO. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol. 1578, pp. 135–149. Springer, Heidelberg (1999)
Hensel, U., Huisman, M., Jacobs, B., Tews, H.: Reasoning about classes in object-oriented languages: Logical models and tools. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 105–121. Springer, Heidelberg (1998)
Hoare, C.A.R.: An Axiomatic Basis of Computer Programming. Communications of the ACM 12, 576–580 (1969)
Hofmann, M., Tang, F.: Generation of verification conditions for Abadi and Leino’s logic of objects. In: Presented at 9th International Workshop on Foundations of Object-Oriented Languages (2002)
Rustan, K., Leino, M.: Recursive object types in a logic of object-oriented programs. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 170–184. Springer, Heidelberg (1998)
Levy, P.B.: Possible world semantics for general storage in call-by-value. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, p. 232. Springer, Heidelberg (2002)
Paulson, L.C.: Logic and Computation: Interactive proof with Cambridge LCF. In: Cambridge Tracts in Theoretical Computer Science, vol. 2 (1987)
Pitts, A.M.: Relational properties of domains. Information and Computation 127, 66–90 (1996)
Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)
Reddy, U.S.: Objects and classes in algol-like languages. Information and Computation 172(1), 63–97 (2002)
Reddy, U.S., Yang, H.: Correctness of data representations involving heap data structures. Science of Computer Programming 50(1–3), 129–160 (2004)
Reus, B.: Class-based versus object-based: A denotational comparison. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 473–488. Springer, Heidelberg (2002)
Reus, B.: Modular semantics and logics of classes. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 456–469. Springer, Heidelberg (2003)
Reus, B., Schwinghammer, J.: Denotational semantics for Abadi and Leino’s logic of objects. Technical Report 2004:03, Informatics, University of Sussex (2004)
Reus, B., Streicher, T.: Semantics and logic of object calculi. Theoretical Computer Science 316, 191–213 (2004)
Reus, B., Wirsing, M., Hennicker, R.: A Hoare-Calculus for Verifying Java Realizations of OCL-Constrained Design Models. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 300–317. Springer, Heidelberg (2001)
von Oheimb, D.: Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience 13(13), 1173–1214 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reus, B., Schwinghammer, J. (2005). Denotational Semantics for Abadi and Leino’s Logic of Objects. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)