Local Reasoning about Programs that Alter Data Structures

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearch

    Peter W. O'Hearn, Queen Mary University of London, United KingdomJohn Clifton Reynolds, United StatesHongseok Yang, Queen Mary, University of London, United KingdomLaurent Fribourg, Denmark
  • 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
Publication year2001
ISBN (print)3-540-42554-3
StatePublished - 2001
EventInternational Workshop on Computer Science Logic - Paris, France
Duration: 10 Sep 200113 Sep 2001
Conference number: 15


ConferenceInternational Workshop on Computer Science Logic

See relations at Aarhus University Citationformats

ID: 283227