Data Structures and Correctness of Programs
Tomasz Kowaltowski · Journal of the ACM · 1979
A techmque for proving correctness of programs manipulating data structures Is proposed.Its three major components are' (i) an abstract representation for the data structures called free state description (FSD), (n) a set of propositions which allow transformations of such FSD's, and (in) semanacs of assignment statements m terms of FSD transformations.The techmque provides a framework for rigorous proofs about programs manipulating data structures with arbitrary sharing of pointers and circularmes Examples of apphcauons include the Deutsch-Schorr-Waite markmg algorithm A grapincal mterpretatzon of proofs is sketched to illustrate the intumve concepts hidden behmd this technique The method extends the one devised by Burstall by allowing arbitrary data structures.