Footprint Logic for Object-Oriented Components

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

doi:10.1007/978-3-031-20872-0_9

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 proceeding › Conference Article in proceeding › Academic › peer-review

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.

Original language	English
Title of host publication	Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings
Editors	Silvia Lizeth Tapia Tarifa, José Proença
Place of Publication	cham
Publisher	Springer
Pages	141-160
Number of pages	20
Volume	13712
Edition	1
ISBN (Electronic)	9783031208720
DOIs	https://doi.org/10.1007/978-3-031-20872-0_9
Publication status	Published - 2 Nov 2022
Event	18th International Conference on Formal Aspects of Component Software - Oslo, Norway Duration: 10 Nov 2022 → 11 Nov 2022 Conference number: 18 https://facs-conference.github.io/2022/

Publication series

Series	Lecture Notes in Computer Science

Conference

Conference	18th International Conference on Formal Aspects of Component Software
Abbreviated title	FACS 2022
Country/Territory	Norway
City	Oslo
Period	10/11/22 → 11/11/22
Internet address	https://facs-conference.github.io/2022/

Keywords

Hoare logic
Invariance
Strong partial correctness

Access to Document

10.1007/978-3-031-20872-0_9

Cite this

Boer, F. S. D., Gouw, S. D., Hiep, H-D. A., & Bian, J. (2022). Footprint Logic for Object-Oriented Components. In S. L. T. Tarifa, & J. Proença (Eds.), Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings (1 ed., Vol. 13712, pp. 141-160). Springer. https://doi.org/10.1007/978-3-031-20872-0_9

Boer, Frank S. de ; Gouw, Stijn de ; Hiep, Hans-Dieter A. et al. / Footprint Logic for Object-Oriented Components. Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings. editor / Silvia Lizeth Tapia Tarifa ; José Proença. Vol. 13712 1. ed. cham : Springer, 2022. pp. 141-160 (Lecture Notes in Computer Science).

@inproceedings{e3ff7cb766074201b73cf1c44e1d5f8a,

title = "Footprint Logic for Object-Oriented Components",

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.",

keywords = "Hoare logic, Invariance, Strong partial correctness",

author = "Boer, {Frank S. de} and Gouw, {Stijn de} and Hiep, {Hans-Dieter A.} and Jinting Bian",

year = "2022",

month = nov,

day = "2",

doi = "10.1007/978-3-031-20872-0_9",

language = "English",

volume = "13712",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "141--160",

editor = "Tarifa, {Silvia Lizeth Tapia} and Jos{\'e} Proen{\c c}a",

booktitle = "Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings",

edition = "1",

note = "18th International Conference on Formal Aspects of Component Software, FACS 2022 ; Conference date: 10-11-2022 Through 11-11-2022",

url = "https://facs-conference.github.io/2022/",

}

Boer, FSD, Gouw, SD, Hiep, H-DA & Bian, J 2022, Footprint Logic for Object-Oriented Components. in SLT Tarifa & J Proença (eds), Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings. 1 edn, vol. 13712, Springer, cham, Lecture Notes in Computer Science, pp. 141-160, 18th International Conference on Formal Aspects of Component Software, Oslo, Norway, 10/11/22. https://doi.org/10.1007/978-3-031-20872-0_9

Footprint Logic for Object-Oriented Components. / Boer, Frank S. de; Gouw, Stijn de; Hiep, Hans-Dieter A. et al.
Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings. ed. / Silvia Lizeth Tapia Tarifa; José Proença. Vol. 13712 1. ed. cham: Springer, 2022. p. 141-160 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - Footprint Logic for Object-Oriented Components

AU - Boer, Frank S. de

AU - Gouw, Stijn de

AU - Hiep, Hans-Dieter A.

AU - Bian, Jinting

N1 - Conference code: 18

PY - 2022/11/2

Y1 - 2022/11/2

N2 - 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.

AB - 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.

KW - Hoare logic

KW - Invariance

KW - Strong partial correctness

U2 - 10.1007/978-3-031-20872-0_9

DO - 10.1007/978-3-031-20872-0_9

M3 - Conference Article in proceeding

VL - 13712

T3 - Lecture Notes in Computer Science

SP - 141

EP - 160

BT - Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings

A2 - Tarifa, Silvia Lizeth Tapia

A2 - Proença, José

PB - Springer

CY - cham

T2 - 18th International Conference on Formal Aspects of Component Software

Y2 - 10 November 2022 through 11 November 2022

ER -

Boer FSD, Gouw SD, Hiep H-DA, Bian J. Footprint Logic for Object-Oriented Components. In Tarifa SLT, Proença J, editors, Formal Aspects of Component Software - 18th International Conference, FACS 2022, Virtual Event, November 10-11, 2022, Proceedings. 1 ed. Vol. 13712. cham: Springer. 2022. p. 141-160. (Lecture Notes in Computer Science). doi: 10.1007/978-3-031-20872-0_9

Footprint Logic for Object-Oriented Components

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this