Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
A Case for Behavior-Preserving Actions in Separation Logic
verfasst von : David Costanzo, Zhong Shao
Erschienen in: Programming Languages and Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Separation Logic is a widely-used tool that allows for local reasoning about imperative programs with pointers. A straightforward definition of this ”local reasoning” is that, whenever a program runs safely on some state, adding more state would have no effect on the program’s behavior. However, for a mix of technical and historical reasons, local reasoning is defined in a more subtle way, allowing a program to lose some behaviors when extra state is added. In this paper, we propose strengthening local reasoning to match the straightforward definition mentioned above. We argue that such a strengthening does not have any negative effect on the usability of Separation Logic, and we present four examples that illustrate how this strengthening simplifies some of the metatheoretical reasoning regarding Separation Logic. In one example, our change even results in a more powerful metatheory.