History-Based Reasoning About Behavioral Subtyping
The work
| Authors | Jinting Bian; Hans-Dieter A. Hiep; Frank S. de Boer |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2024 |
| Citekey | bian2024historybased |
Where it appeared
| Published in | Theoretical Aspects of Computing |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Pages | 331--349 |
Identifiers
| DOI | 10.1007/978-3-031-77019-7_19 |
|---|---|
| OpenAlex | W4404575057 |
Access
| Landing page | https://doi.org/10.1007/978-3-031-77019-7_19 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | bian2026historybased |
|---|
Abstract
We introduce a new history-based proof-theory for reasoning about behavioral subtyping in class and interface hierarchies. Our approach is based on a semantic definition of types in terms of sets of sequences of method calls and returns, so-called histories. Behavioral subtyping is then naturally defined semantically as a set-theoretic subset relation between sets of histories, modulo a projection relation that captures the syntactic subtype relation. The main contribution is a Hoare-style proof theory for the specification and verification of the behavioral subtyping relation in terms of histories, abstracting from the underlying implementation. Through the use of a banking example we show the practical applicability of our approach.
Cite it as
@inproceedings{bian2024historybased,
title = {History-Based Reasoning About Behavioral Subtyping},
author = {Jinting Bian and Hans-Dieter A. Hiep and Frank S. de Boer},
year = {2024},
booktitle = {Theoretical Aspects of Computing},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {331--349},
doi = {10.1007/978-3-031-77019-7_19},
}
This record lives at https://refs.drheap.org/bian2024historybased/ and will keep doing so.