FACS 2022

Logics & Semantics

Footprint Logic for Object-Oriented Components

Frank de Boer, Hans Dieter Hiep, Jinting Bian, Stijn de Gouw

on  Fri, 11:00in  Zoomfor  30min

Presenter: Hans Dieter Hiep
Session Chair: Clemens Dubslaff

We introduce a new way of reasoning about invariance in terms of footprints in a Hoare 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. Invariance of an assertion is ensured by means of a form of bounded quantification which excludes references to a given footprint.

 Overview  Program