FURTHER REASONING ABOUT SHARED MUTABLE DATA STRUCTURE

John C. Reynolds

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.