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.
CITATION STYLE
Abadi, M., & M. Leino, K. R. (1997). A logic of object-oriented programs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1214, pp. 682–696). Springer Verlag. https://doi.org/10.1007/bfb0030634
Mendeley helps you to discover research relevant for your work.