John C. Reynolds
Carnegie Mellon University
Separation Logic: A Logic for Shared Mutable Data Structures
Abstract:
In joint work with
Peter O'Hearn and others, based on early ideas of Burstall, we have
developed
an extension of Hoare logic that permits reasoning about low-level
imperative
programs that use 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
of storage. Assertions are extended by introducing a ``separating
conjunction'' that asserts that its subformulas hold for disjoint parts
of the
heap, and a closely related "separating implication". 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 paper, we will
survey the current development of this program logic, including
extensions that
permit unrestricted address arithmetic, dynamically allocated arrays,
and
recursive procedures. We will also discuss promising future
directions.
KEYWORDS:
separation logic, shared data structures, mutable data structures,
Hoare logic,
logic of bunched implications, separating conjunction, separating
implication,
address arithmetic, program specification, program verification.
Principles
of Programming Seminars
Friday, January 24, 2003
3:30 p.m.
Wean Hall 8220