Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Dinsdale-Young:2011:10.1007/978-3-642-22944-2_3,
author = {Dinsdale-Young, T and Gardner, P and Wheelhouse, M},
doi = {10.1007/978-3-642-22944-2_3},
pages = {36--39},
publisher = {Springer Verlag},
title = {Abstract local reasoning for program modules},
url = {http://dx.doi.org/10.1007/978-3-642-22944-2_3},
year = {2011}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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. © 2011 Springer-Verlag.
AU  - Dinsdale-Young,T
AU  - Gardner,P
AU  - Wheelhouse,M
DO  - 10.1007/978-3-642-22944-2_3
EP  - 39
PB  - Springer Verlag
PY  - 2011///
SN  - 0302-9743
SP  - 36
TI  - Abstract local reasoning for program modules
UR  - http://dx.doi.org/10.1007/978-3-642-22944-2_3
UR  - http://hdl.handle.net/10044/1/33222
ER  -
Download