Data Structures and Correctness of Programs

Abstract

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 FSDs, 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. © 1979, ACM. All rights reserved.