Further Reasoning about Shared Mutable Data Structure

John C. Reynolds, Carnegie Mellon University and BRICS, Aarhus

In joint work with Peter O'Hearn and Hongseok Yang, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about shared mutable data structure.

The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation. Assertions are extended by introducing an independent conjunction operation that asserts that its subformulas hold for disjoint parts of the heap. Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing.

In this talk, we will introduce the basic concepts of our approach. Then we will describe several recent extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures.