Local Reasoning about Programs that Alter Data Structures

Publication: ResearchArticle in proceedings

  • Peter W. O'Hearn
    Peter W. O'HearnQueen Mary University of LondonUnited Kingdom
  • John Clifton Reynolds
    John Clifton ReynoldsUnited States
  • Hongseok Yang
    Hongseok YangQueen Mary, University of LondonUnited Kingdom
  • Laurent Fribourg
    Laurent FribourgDenmark
  • Department of Computer Science

We describe an extension of Hoare's logic for reasoning about programs that alter data structures. We consider a low-level storage model based on a heap with associated lookup, update, allocation and deallocation operations, and unrestricted address arithmetic. The assertion language is based on a possible worlds model of the logic of bunched implications, and includes spatial conjunction and implication connectives alongside those of classical logic. Heap operations are axiomatized using what we call the \small axioms", each of which mentions only those cells accessed by a particular command. Through these and a number of examples we show that the formalism supports local reasoning: A speci-cation and proof can concentrate on only those cells in memory that a program accesses.

This paper builds on earlier work by Burstall, Reynolds, Ishtiaq and O'Hearn on reasoning about data structures.

Original languageEnglish
Title of host publicationInternational Workshop on Computer Science Logic : Lecture Notes in Computer Science
Number of pages20
Volume2142
PublisherSpringer
Publication year2001
Pages1-19
ISBN (print)3-540-42554-3
StatePublished - 2001
Event - Paris, France

Conference

ConferenceInternational Workshop on Computer Science Logic
Nummer15
LandFrance
ByParis
Periode10/09/200113/09/2001

See relations at Aarhus University Citationformats

ID: 283227