2022
Footprint logic for object-oriented components
Publication
Publication
Presented at the
Formal Aspects of Component Software. FACS 2022 (November 2022), Virtual
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.
| Additional Metadata | |
|---|---|
| , , | |
| doi.org/10.1007/978-3-031-20872-0_9 | |
| Lecture Notes in Computer Science | |
| Formal Aspects of Component Software. FACS 2022 | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
de Boer, F., de Gouw, S., Hiep, H.-D., & Bian, J. (2022). Footprint logic for object-oriented components. In Proceedings of the 18th International Conference on Formal Aspects of Component Software, FACS 2022 (pp. 141–160). doi:10.1007/978-3-031-20872-0_9 |
|
