Advertisement
Published in:
2012 | OriginalPaper | Chapter
A Case for Behavior-Preserving Actions in Separation Logic
Authors : David Costanzo, Zhong Shao
Published in: Programming Languages and Systems
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. 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.