Abstraction and refinement for local reasoning

Abstract

Local reasoning has become a well-established technique in program verification, which has been shown to be useful at many different levels of abstraction. In separation logic, we use a low-level abstraction that is close to how the machine sees the program state. In context logic, we work with high-level abstractions that are close to how the clients of modules see the program state.We apply program refinement to local reasoning, demonstrating that high-level local reasoning is sound for module implementations.We consider two approaches: one that preserves the high-level locality at the low level; and one that breaks the high-level 'fiction' of locality. © 2010 Springer-Verlag Berlin Heidelberg.