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.

REFERENCES

• 1: Burstall, R. M., Some Techniques for Proving Correctness of Programs which Alter Data Structures. Machine Intelligence 7, 1972.
• 2: Cook, S. A., Axiomatic and Interpretive Semantics for an Algol Fragment. Course notes for CSC 2409S, Dept. of Computer Science, University of Toronto, March 1974.
• 3: Davis, M., Computability and Unsolvability. McGraw-Hill, 1958.
• 4: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 5: Kowaltowski, T., Correctness of Programs Manipulating Data Structure. Memorandum No. ERL-M404, Electronics Research Laboratory, University of California, Berkeley, September 1973.
• 6: Laventhal, M. S., Verification of Programs Operating on Structured Data. M.Sc. Thesis, M.I.T., February 1974.
• 7: Morris, J. H., Verification Oriented Language Design. Technical Report 7, Dept. of Computer Science, University of California, Berkeley, December 1972.
• 8: Rosenberg, A. L., Data Graphs and Addressing Schemes. Journal of Computer and System Sciences, June 1971, pp. 193-238.
• 9: Standish, T. A., Data Structures: An Axiomatic Approach. Automatic Programming Memo 3, Bolt, Beranek and Newman Inc., August 1973.