Abstract Local Reasoning for Program Modules
Venue
Proceedings of the 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11), pp. 36–39
Publication Year
2011
Identifiers
Authors
- Thomas Dinsdale-Young
- Philippa Gardner
- Mark J. Wheelhouse
Abstract
Hoare logic ([7]) is an important tool for formally proving correctness properties of programs. It takes advantage of modularity by treating program fragments in terms of provable specifications. However, heap programs tend to break this type of modular reasoning by permitting pointer aliasing. For instance, the specification that a program reverses one list does not imply that it leaves a second list alone. To achieve this disjointness property, it is necessary to establish disjointness conditions throughout the proof.