zbMATH — the first resource for mathematics

A logic of object-oriented programs. (English) Zbl 1274.68055
Dershowitz, Nachum (ed.), Verification: Theory and practice. Essays dedicated to Zohar Manna on the occasion of his 64th birthday. Berlin: Springer (ISBN 3-540-21002-4/pbk). Lecture Notes in Computer Science 2772, 11-41 (2003).
Summary: 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.
For the entire collection see [Zbl 1045.68009].
Reviewer: Reviewer (Berlin)

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
03B70 Logic in computer science
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI