Traditional Hoare logic is an important tool for proving the correctness of programs. However, with heap programs, it is not possible to use this reasoning in a modular way. This is because it is necessary to account for the possibility of multiple references to the same data. For example, a proof that a program reverses a list cannot be used to establish that a second, disjoint list is unchanged; disjointness conditions must be explicitly added at every step in the proof.

Building on Hoare logic, O'Hearn, Reynolds and Yang addressed this problem by introducing separation logic for reasoning locally about heap programs. The fundamental principle of local reasoning is that, if we know how a local computation behaves on some state, then we can infer the behaviour when the state is extended: it simply leaves the additional state unchanged. Separation logic achieves local reasoning by treating state as resource. A program is specified in terms of its footprint – the resource necessary for it to operate – and a frame rule is used to infer that any additional resource is indeed unchanged. For example, given a proof that a program reverses a list, the frame rule can directly establish that the program leaves a second, disjoint list alone. Consequently, separation logic enables modular reasoning about heap programs.

Abstraction and refinement are also essential for modular reasoning. Abstraction takes a concrete program and produces an abstract specification; refinement takes an abstract specification and produces a correct implementation. Both approaches result in a program that correctly implements an abstract specification. Such a result essential for modularity because it means that a program can be replaced by any other program that meets the same specification. Abstraction and refinement are well-established techniques in program verification, but have so far not been fully understood in the context of local reasoning.