An approach to the implementation and verification of abstract data
Chien‐Chiao Yang, Ming‐Lien Lee · Journal of the Chinese Institute of Engineers · 1986
The concept of abstraction can be used to simplify and formalize the design of software. However, most of the existing techniques based on abstraction only consider the control structure but not the data structures in the software. The transformation of a data abstraction, i.e., an abstract data type, to a physical data structure is a complicated process. It is composed of three major parts: a specification technique for describing a data abstraction; a deriving process for deriving the representation of the abstraction based on the specification; and a verification method for verifying the correctness of the specification and the representation of the abstraction. In this paper, we will concentrate on the last two problems, and it is assumed that the algebraic specification technique is used for describing abstract data types. Also, we will use examples to illustrate the use of the proposed approach.