A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts
The work
| Authors | Cees Pierik; Frank S. de Boer |
|---|---|
| Type | inproceedings |
| Year | 2003 |
| Citekey | pierik2003syntaxdirected |
Where it appeared
| Published in | Formal Methods for Open Object-Based Distributed Systems |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 2884 |
| Pages | 64--78 |
Identifiers
| DOI | 10.1007/978-3-540-39958-2_5 |
|---|---|
| OpenAlex | W1620267008 |
Access
| Landing page | https://doi.org/10.1007/978-3-540-39958-2_5 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/978-3-540-39958-2_5.pdf |
Abstract
This paper outlines a sound and complete Hoare logic for a sequential object-oriented language with inheritance and subtyping like Java. It describes a weakest precondition calculus for assignments and object-creation, as well as Hoare rules for reasoning about (mutually recursive) method invocations with dynamic binding. Our approach enables reasoning at an abstraction level that coincides with the general abstraction level of object-oriented languages.
A copy is held
pdf, 210.4 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-18 16:22 UTC |
Filed under
Cite it as
@inproceedings{pierik2003syntaxdirected,
title = {A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts},
author = {Cees Pierik and Frank S. de Boer},
year = {2003},
booktitle = {Formal Methods for Open Object-Based Distributed Systems},
pages = {64--78},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-540-39958-2_5},
}
This record lives at https://refs.drheap.org/pierik2003syntaxdirected/ and will keep doing so.