Personal tools
You are here: Home Events Abstract Archives 2001 Local Reasoning about Shared Mutable Data Structure

Local Reasoning about Shared Mutable Data Structure

Peter O'Hearn Queen Mary, University of London 4pm, Thursday 3 May 2001 Room 2511, JCMB, King's Buildings

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 addressed by natural numbers, with associated lookup, update, allocation and deallocation operations, and arbitrary address arithmetic. The logic includes a spatial conjunction and spatial implication, which are used to decompose and compose specifications according to the areas of memory they refer to. We show how the formalism supports local reasoning: a specification and proof can concentrate on only those cells in memory that a program accesses. This is made possible using a rule for introducing frame axioms, which enables invariant properties for memory that a program does not access to be inferred automatically.

This talk describes work with John Reynolds and Hongseok Yang.

Document Actions