History-based reasoning about behavioral subtyping (extended paper)
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep; Frank S. de Boer |
|---|---|
| Editors | |
| Type | article |
| Year | 2026 |
| Citekey | bian2026historybased |
Where it appeared
| Published in | Theoretical Computer Science |
|---|---|
| Publisher | Elsevier BV |
| Volume | 1071 |
| Pages | 115847 |
Identifiers
| DOI | 10.1016/j.tcs.2026.115847 |
|---|---|
| OpenAlex | W7133883109 |
Access
| Landing page | https://doi.org/10.1016/j.tcs.2026.115847 |
|---|
Abstract
We introduce a new history-based proof method for reasoning about behavioral subtyping in class and interface hierarchies. Our approach is based on histories: sequences where method calls and their corresponding returns are recorded as a single event. Behavioral subtyping is then defined semantically as a relation between sets of histories, modulo a projection relation that captures the syntactic inheritance relation. The main contribution is a Hoare-style proof theory for the specification and verification of object-oriented programs, allowing one to reason also about interfaces where one abstracts from the state of the underlying implementation. Through the use of a banking example we show the practical applicability of our approach. Open Science. Includes a source code artifact [45].
How it got here
| How it got here | import via drheap-program-correctness |
|---|---|
| Added | 2026-08-23 00:00 UTC |
| Approved by | a person 2026-08-24 07:32 UTC |
Filed under
Cite it as
@article{bian2026historybased,
title = {History-based reasoning about behavioral subtyping (extended paper)},
author = {Jinting Bian and Hans-Dieter A. Hiep and Frank S. de Boer},
year = {2026},
journal = {Theoretical Computer Science},
publisher = {Elsevier BV},
volume = {1071},
pages = {115847},
doi = {10.1016/j.tcs.2026.115847},
}
This record lives at https://refs.drheap.org/bian2026historybased/ and will keep doing so.