Reasoning About Shared Mutable Data Structure

Drawing on early work by Burstall, we extend Hoare's approach to the partial correctness of imperative programs to deal with programs that perform destructive updates to data structures containing more than one pointer to the same location. The key concept is an "independent conjunction" P & Q, which only holds when P and Q are both true and depend upon distinct areas of storage. Exemplary proofs are given of simple programs that manipulate singly and doubly linked lists.

LS Home page or Talks in 1998/99