Constructing a theory of a data structure as an aid to program development. (English) Zbl 0382.68029

Summary: 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.


68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI