A formal semantics for isorecursive and equirecursive state abstractions
Alexander J. Summers, Sophia Drossopoulou · Repository for Publications and Research Data (ETH Zurich) · 2012
Methodologies for static program verication and analysis often support recursive predicates in specications, in order to reason about recursive data structures. Intuitively, a predicate instance represents the complete unrolling of its denition; this is the equirecursive interpretation. However, this semantics is unsuitable for static veri- cation, when the recursion becomes unbounded. For this reason, most static veriers dierentiate between, e.g., a predicate instance and its corresponding body, while providing a facility to map between the two; this is the isorecursive semantics. While this latter interpretation is usually implemented in practice, only the equirecursive semantics is typically treated in theoretical work. In this paper, we provide both an isorecursive and an equirecursive formal semantics for recursive denitions in the context of Chalice, a veri cation methodology based on implicit dynamic frames. We show that development of such formalisations requires addressing several subtle issues, such as the possibility of innitely-recursive denitions and the need for the isorecursive semantics to correctly re ect the restrictions that make it readily implementable. These questions are made more challenging still in the context of implicit dynamic frames, where the use of heap-dependent expressions provides further pitfalls for a correct formal treatment.