Data structure implementation and correctness

Abstract

<p>Recently, implementation of data structures and correctness proofs of data structure implementations have become important problems in the construction of data abstraction languages, data base systems, and software engineering. The research reported here is primarily concerned with the definition and implementation of data structures, and how to prove an implementation correct;This thesis develops a general technique to implement the source data structure (d1) in terms of the target data structures (d2). That is, given data structures d1 and d2, an implementation of d1 by d2 is defined separately on the syntactical and semantical levels of data structure elements. This work makes a sharp distinction between the specification of a data structure and its implementation. Specification of data structures is considered to be abstract, that is, implementation independent of any specific programming language;This thesis deals primarily with developing criteria for providing provably correct implementation of data structures. The correctness of data structure implementation is developed on two levels: syntactical and semantical. Syntactically, correct implementations deal with algebraic equations (conditional and unconditional) that specify a data structure, while the semantically correct implementations define correctness on the basis of the semantic algebra in the data structure specifications. All the implementations are specified by tree transducers, reducing the problem of implementation to a problem of translation;The issue of tree transducers is addressed on the syntactic and semantic levels. Two key syntactical properties of tree transducers have been investigated. They are, the "consistency" and "semiconsistency" of tree transducers with respect to the algebraic equations defining the source and target data structures. These properties have been used for the syntactical correctness proof of the implementation of data structures. One of the key results of this thesis is the development of "syntactically honest" tree transducers, which is based on a lattice. It has been proved that syntactically honest tree transducers form a base for syntactically correct implementation of data structures.</p>