An Example of Local Reasoning in BI Pointer Logic: the Schorr−Waite Graph Marking Algorithm
Hongseok Yang · 2001
Reasoning about programs manipulating pointers has been considered as difficult not because of the lack of formalisms for verifying pointer programs, but because of the significant increase in the complexity of proofs in each formalism over an informal argument. Recently, there has been noticeable development in handling the complexity by exploiting locality of memory access within a code fragment. Reynolds introduced a pointer logic based on a "spatial" interpretation, where different parts of a formula refer to different area of memory; this holds the promise of managing complexity of aliasing information. O'Hearn proposed a "tight" interpretation of Hoare triples which reflects locality of memory access: in addition to the usual requirement of Hoare triples, a command is required to access only those memory cells "mentioned" in a precondition. These two ideas are combined in the Frame