License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.EVCS.2023.11
URN: urn:nbn:de:0030-drops-177812
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17781/
Go to the corresponding OASIcs Volume Portal

Greenberg, Michael

Reasoning About Paths in the Interface Graph

pdf-format:
OASIcs-EVCS-2023-11.pdf (0.7 MB)

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 [Christos Dimoulas et al., 2011; Christos Dimoulas et al., 2012] - 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.

BibTeX - Entry

@InProceedings{greenberg:OASIcs.EVCS.2023.11,
  author =	{Greenberg, Michael},
  title =	{{Reasoning About Paths in the Interface Graph}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{11:1--11:11},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17781},
  URN =		{urn:nbn:de:0030-drops-177812},
  doi =		{10.4230/OASIcs.EVCS.2023.11},
  annote =	{Keywords: interfaces, components, lambda calculus, dynamic analysis}
}

Keywords: interfaces, components, lambda calculus, dynamic analysis
Collection: Eelco Visser Commemorative Symposium (EVCS 2023)
Issue Date: 2023
Date of publication: 21.03.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI