Constructing a theory of a data structure as an aid to program development

Abstract

This paper illustrates an extension to the method of developing programs via abstract data types. In order to make the proofs shorter and more intuitive a collection of lemmas (theory) is constructed for the main data types (trees). The problem used as an example is the recording of equivalence relations, one of the programs given is based on the Fischer-Galler algorithm. © 1979 Springer-Verlag.