A logic of object-oriented programs
The work
| Authors | Martín Abadi; K. Rustan M. Leino |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1997 |
| Citekey | abadi1997logic |
Where it appeared
| Published in | TAPSOFT '97: Theory and Practice of Software Development |
|---|---|
| Publisher | Springer |
| Pages | 682--696 |
Identifiers
| DOI | 10.1007/bfb0030634 |
|---|---|
| OpenAlex | W1945350451 |
Access
| Landing page | https://doi.org/10.1007/bfb0030634 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/BFb0030634.pdf |
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.
A copy is held
pdf, 783.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-16 15:22 UTC |
Filed under
Cite it as
@inproceedings{abadi1997logic,
title = {A logic of object-oriented programs},
author = {Martín Abadi and K. Rustan M. Leino},
year = {1997},
booktitle = {TAPSOFT '97: Theory and Practice of Software Development},
publisher = {Springer},
pages = {682--696},
doi = {10.1007/bfb0030634},
}
This record lives at https://refs.drheap.org/abadi1997logic/ and will keep doing so.