Footprint Logic for Object-Oriented Components

Frank S. de Boer*, Stijn de Gouw*, Hans-Dieter A. Hiep*, Jinting Bian

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference Article in proceedingAcademicpeer-review


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.

Original languageEnglish
Title of host publicationFormal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings
EditorsSilvia Lizeth Tapia Tarifa, José Proença
Place of Publicationcham
Number of pages20
ISBN (Electronic) 9783031208720
Publication statusPublished - 2 Nov 2022
Event18th International Conference on Formal Aspects of Component Software - Oslo, Norway
Duration: 10 Nov 202211 Nov 2022
Conference number: 18

Publication series

SeriesLecture Notes in Computer Science


Conference18th International Conference on Formal Aspects of Component Software
Abbreviated titleFACS 2022
Internet address


  • Hoare logic
  • Invariance
  • Strong partial correctness


Dive into the research topics of 'Footprint Logic for Object-Oriented Components'. Together they form a unique fingerprint.

Cite this