Local Reasoning with First-Class Heaps, and a New Frame Rule
Duc-Hiep Chu, Joxan Jaffar · arXiv (Cornell University) · 2015
Separation Logic (SL) brought an advance to program verification of data structures by interpreting (recursively defined) predicates as implicit heaps, and using a separating conjoin operator to construct heaps from disjoint subheaps. While the Frame Rule of SL facilitated local reasoning in program fragments, its restriction to disjoint subheaps means that any form of sharing between predicates is problematic. With this as background motivation, we begin with an assertion language in which subheaps may be explicitly defined within predicates, and the effect of separation obtained by specifying that certain heaps are disjoint. The strength of this base language is not just its expressiveness, but it is amenable to symbolic execution and therefore automatic program verification. In this paper, we extend this base language with a new frame rule to accommodate subheaps and nonseparating conjoining of subheaps so as to provide compositional reasoning. This significantly extends both the expressiveness and automatability of the base language. Finally we demonstrate our framework to automatically prove two significant example programs, one concerning a summary of a program fragments, and one exhibiting structure sharing in data structures.