A case study of abstract implementations and their correctness

Abstract

A new implementation concept for algebraic specification languages supports hierarchical programming mainly because it provides a semantical basis for correctness proofs. "Abstract programs" describe syntactically how data and operations of a lower level data type should represent those of an upper level type. Dependent on these programs a general semantical construction transforms the lower level type into an implementation of the upper level type. The implementation is correct if the result of this construction coincides with the semantics of the upper level type. Therefore this concept involves a clear distinction between the syntactical and the semantical part of an abstract implementation. Although the syntax of such an implementation always supplies a "freely generated" semantics, the concept also admits the use of other (algebraic) models which often ease correctness proofs. A data type for performing some text analysis is specified and implemented by arrays which are accessed via an efficient hashing technique. Moreover, we give a correctness proof of this implementation that partly refers to correctness criteria introduced in an earlier paper where the whole concept is discussed in more detail.