Research output: Research › Article in proceedings

- Peter W. O'HearnPeter W. O'HearnQueen Mary University of LondonUnited Kingdom
- John Clifton ReynoldsJohn Clifton ReynoldsUnited States
- Hongseok YangHongseok YangQueen Mary, University of LondonUnited Kingdom
- Laurent FribourgLaurent 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 language | English |
---|---|

Title of host publication | International Workshop on Computer Science Logic : Lecture Notes in Computer Science |

Number of pages | 20 |

Volume | 2142 |

Publisher | Springer |

Publication year | 2001 |

Pages | 1-19 |

ISBN (print) | 3-540-42554-3 |

State | Published - 2001 |

Event | International Workshop on Computer Science Logic - Paris, France Duration: 10 Sep 2001 → 13 Sep 2001 Conference number: 15 |

Conference | International Workshop on Computer Science Logic |
---|---|

Nummer | 15 |

Land | France |

By | Paris |

Periode | 10/09/2001 → 13/09/2001 |

See relations at Aarhus University Citationformats

ID: 283227