The FLINT Project








A Case for Behavior-Preserving Actions in Separation Logic

Last modified: Thu Dec 13 02:51:08 2012 GMT.


David Costanzo
Zhong Shao


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, any additional state has no effect on the program's behavior. In the presence of nondeterminism, however, local reasoning must be defined as something more subtle; specifically, additional state is allowed to decrease the amount of nondeterminism of the program. This subtlety causes difficulty in proving various metatheoretical facts about Separation Logic and its variants. Four specific examples are: (1) specifying the behavior of a program on its minimal footprint does not provide a complete specification; (2) data refinement requires a rather unintuitive restriction that the memory used by an abstract module be a subset of the memory used by a concrete module refining the abstract one; (3) Relational Separation Logic requires quite a bit of additional work to prove the frame rule sound; and (4) it is quite tricky to define a model of Separation Logic in which the total domain of memory is finite. In this paper, we show how to cleanly resolve all of these issues by strengthening the definition of local reasoning to eliminate the subtlety. We contend that this solution will also similarly resolve future metatheoretical issues.


Copyright © 1996-2023 The FLINT Group <flint at cs dot yale dot edu>
Yale University Department of Computer Science
Validate this page