Reasoning About Paths in the Interface Graph

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

Abstract

Clearly specified interfaces between software components are invaluable: development proceeds in parallel; implementation details are abstracted away; invariants are enforced; code is reused. But this abstraction comes with a cost: well chosen interfaces let related tasks be grouped together, but a running program interleaves tasks of all kinds. Reasoning about which values cross a given interface or which interfaces a value will cross is challenging. It is particularly hard to know that interfaces apply runtime enforcement mechanisms correctly: as programs run, values cross abstraction boundaries in subtle ways. One particular case of such reasoning – proving that a contract system checks contracts correctly at runtime [2, 3] – uses a dynamic analysis to keep track of which interfaces are responsible for which values. The dynamic analysis works by giving an alternative semantics that “colors” values to match the components responsible for them. No program is ever run in this alternative semantics – it’s a formal tool to verify that the contract system’s enforcement is correct. In this short paper, we refine Dimoulas et al.’s dynamic analysis to more precisely track colors, phrasing our results graph theoretically: a value’s colors are a path in the interface graph of the original program. Our graph theoretic framing makes it easy to see that the dynamic analysis is subsumed by Eelco Visser’s scope graphs.

Original languageEnglish
Title of host publicationEelco Visser Commemorative Symposium, EVCS 2023
EditorsRalf Lammel, Peter D. Mosses, Friedrich Steimann
ISBN (Electronic)9783959772679
DOIs
StatePublished - 1 Mar 2023
Event2023 Eelco Visser Commemorative Symposium, EVCS 2023 - Delft, Netherlands
Duration: 5 Apr 2023 → …

Publication series

NameOpenAccess Series in Informatics
Volume109
ISSN (Print)2190-6807

Conference

Conference2023 Eelco Visser Commemorative Symposium, EVCS 2023
Country/TerritoryNetherlands
CityDelft
Period5/04/23 → …

Keywords

  • components
  • dynamic analysis
  • interfaces
  • lambda calculus

Fingerprint

Dive into the research topics of 'Reasoning About Paths in the Interface Graph'. Together they form a unique fingerprint.

Cite this