Footprint Logic for Object-Oriented Components (extended paper)
Formal Aspects of Computing, vol. 37, pp. 1–23
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.
Authors 4
-
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands
Centrum Wiskunde en Informatica, Amsterdam, Netherlands
Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands
-
Centrum Wiskunde & Informatica · Open University of the Netherlands
Affiliation as printed
Open University of The Netherlands, Heerlen, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands
Centrum Wiskunde en Informatica, Amsterdam Netherlands
Open University of The Netherlands, Heerlen, Netherlands
-
Hans-Dieter A. Hiep Aachen Centrum Wiskunde & Informatica Netherlands and Leiden Institute of Advanced Computer Science (LIACS) Leiden Institute of Advanced Computer Science
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Centrum Wiskunde & Informatica, Amsterdam, Netherlands and Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands
Centrum voor Wiskunde en Informatica, Amsterdam Netherlands
Leiden Institute of Advanced Computer Science, Leiden University, Leiden Netherlands
-
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands
Centrum Wiskunde en Informatica, Amsterdam Netherlands
Leiden Institute of Advanced Computer Science, Leiden University, Leiden Netherlands
Cited by 0 stored of 0
No patents citing this paper on Lens.org (checked 2026-10-11).