Abstract
We develop a logic for reasoning about object-oriented programs. The logic is for a language with an imperative semantics and aliasing, and accounts for self-reference in objects. It is much like a type system for objects with subtyping, but our specifications go further than types in detailing pre- and postconditions. We intend the logic as an analogue of Hoare logic for object-oriented programs. Our main technical result is a soundness theorem that relates the logic to a standard operational semantics. © Springer-Verlag Berlin Heidelberg 2003.
Cite
CITATION STYLE
Abadi, M., & Leino, K. R. M. (2004). A logic of object-oriented programs. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2772, 11–41. https://doi.org/10.1007/978-3-540-39910-0_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
