An assertion language for data structures

Abstract

In this paper we wish to consider the problem of proving assertions about programs that construct and alter arbitrarily complex data structures. In recent years several papers have been written on the subject of proving assertions about such programs; however, the class of data structures considered has generally been a proper sub-class of the class of all data structures, such as the classes of linear lists or trees. [Burstall 1972] discusses the problem of what he calls Distinct Non-repeating Lists and Distinct Non-repeating Trees. [Kowaltowski 1973] extends Burstall's approach. His approach is likewise basically tree-oriented but is applicable to more general data structures. [Laventhal 1974] restricts his attention to 'simple singly-linked lists', noting the problem of providing 'a complete framework for correctness proofs' if one attempts to handle very general data structures. [Morris 1972] discusses the question of designing a programming language for general data structures in order to facilitate verification of programs written in such a language. [Standish 1973] provides a set of axioms for the class of data structures in which, for instance, two data structures are equal iff they are component-wise equal.