Correctness proofs for abstract implementations

New syntax and semantics for implementation of abstract data types are presented in this paper. This formalism leads to a simple, exhaustive description of the abstract implementation correctness criteria. These correctness criteria are expressed in terms of sufficient completeness and hierarchical consistency. Thus, correctness proofs of abstract implementations can be handled using classical tools such as term rewriting methods, structural induction methods, or syntactical methods (e. g. , fair presentations). The main idea of this approach is a fundamental distinction between descriptive and constructive specifications, using both abstraction and representation functions. Moreover, we show that the composition of several correct abstract implementations is always correct. This provides a formal foundation for a methodology of program development by stepwise refinement.

Authors

• Gilles Bernot

Keywords

No keywords are indexed for this paper.