Data structure implementation and correctness

Thumbnail Image
Parsian, Mahmoud
Major Professor
Committee Member
Journal Title
Journal ISSN
Volume Title
Research Projects
Organizational Units
Organizational Unit
Computer Science

Computer Science—the theory, representation, processing, communication and use of information—is fundamentally transforming every aspect of human endeavor. The Department of Computer Science at Iowa State University advances computational and information sciences through; 1. educational and research programs within and beyond the university; 2. active engagement to help define national and international research, and 3. educational agendas, and sustained commitment to graduating leaders for academia, industry and government.

The Computer Science Department was officially established in 1969, with Robert Stewart serving as the founding Department Chair. Faculty were composed of joint appointments with Mathematics, Statistics, and Electrical Engineering. In 1969, the building which now houses the Computer Science department, then simply called the Computer Science building, was completed. Later it was named Atanasoff Hall. Throughout the 1980s to present, the department expanded and developed its teaching and research agendas to cover many areas of computing.

Dates of Existence

Related Units

Journal Issue
Is Version Of

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.

Subject Categories
Fri Jan 01 00:00:00 UTC 1982