John C. Reynolds
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.
September 8, 1999
3:30pm
Wean 8220