A Logic of Object-Oriented Programs

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.

• Type: Conference
• Year: 2003
• Where: BIRTHDAY
• Authors: Martín Abadi, K. Rustan M. Leino
• Keywords: Applied Computing, BIRTHDAY 2003, Hoare Logic, Logic, Object-oriented Programs