Footprint Logic for Object-Oriented Components (extended paper)
The work
| Authors | Frank S. de Boer; Stijn de Gouw; Hans-Dieter Hiep; Jinting Bian |
|---|---|
| Editors | |
| Type | article |
| Year | 2025 |
| Citekey | boer2025footprint |
Where it appeared
| Published in | Formal Aspects of Computing |
|---|---|
| Publisher | Association for Computing Machinery |
| Volume | 37 |
| Issue | 2 |
| Pages | 11:1--11:23 |
Identifiers
| DOI | 10.1145/3703921 |
|---|---|
| OpenAlex | W4404542366 |
Access
| Landing page | https://doi.org/10.1145/3703921 |
|---|---|
| Free full text | https://dl.acm.org/doi/pdf/10.1145/3703921 |
Related
| Distinct from | boer2022footprint |
|---|---|
| Distinct from | broy2024does |
Abstract
We introduce a new way of reasoning about invariance in terms of footprints in a program logic for object-oriented components. A footprint of an object-oriented component is formalized as a monadic predicate that describes which objects on the heap can be affected by the execution of the component. Assuming encapsulation, this amounts to specifying which objects of the component can be called. Adaptation of local specifications into global specifications amounts to showing invariance of assertions, which is ensured by means of a form of bounded quantification which excludes references to a given footprint. The new approach is compared to two existing approaches to reason about invariance: separation logic and dynamic frames.
Cite it as
@article{boer2025footprint,
title = {Footprint Logic for Object-Oriented Components (extended paper)},
author = {Frank S. de Boer and Stijn de Gouw and Hans-Dieter Hiep and Jinting Bian},
year = {2025},
journal = {Formal Aspects of Computing},
publisher = {Association for Computing Machinery},
volume = {37},
number = {2},
pages = {11:1--11:23},
doi = {10.1145/3703921},
}
This record lives at https://refs.drheap.org/boer2025footprint/ and will keep doing so.