A BRICS Mini-Course
June 18, 20 and 22, 2001
John C. Reynolds, John.Reynolds@cs.cmu.edu
Computer Science Department, Carnegie Mellon University, Pittsburgh, USA
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.
Having introduced our low-level programming language and the language of assertions, we will develop inference rules for program specifica- tions and annotated programs. Then, we will prove a variety of exem- plary programs for list and tree manipulation, and consider extensions of our logic.
Exercises and answers are available from my web page under the heading "Lectures on Reasoning about Shared Mutable Data Structures".