Separation logic’s strength is that it let’s you reason locally about heap-manipulating programs by letting you split the heap into disjoint parts. But some data structures don’t easily split into parts and you have to maintain global consistency properties across the structure because they “use mutation and assignment as a way of globally broadcasting information to the rest of the program state.” This paper tackles an example of such a structure: an instance of the subject-observer pattern like that found in a spreadsheet where each node contains a list of the nodes it depends on and also of the nodes that depend on it so that, when a node changes value, nodes that depend on it can be invalidated/updated.
The approach taken in this paper has many parts
-
Push the “frame rule” of separation logic into each inference rule by making all rules universally quantified over possible extensions of the heap.
-
Define a small domain-specific separation logic specifically for reasoning about cell networks.
-
The big problem is that a change in one part of the heap can change the interpretation of other parts of the heap. To tackle this, they define a “ramification operator” that transforms the rest of the heap to match that change in interpretation. (This operator is specific to cell networks.)
This approach is then applied to the task of verifying an imperative implementation of Functional Reactive Programming by reasoning about an (inefficient) pure implementation of causal stream transducers and an imperative implementation based on cell networks.
Papers related to Verifying event-driven programs using ramified frame properties
- The ramifications of sharing in data structures [hobor:popl:2013]