Correctness and Extension of Specifications

This chapter deals with the question of how to prove that a specification is correct w.r.t. a given data type. Since correctness proofs are usually a lengthy and nontrivial task, but are of extraordinary importance if one wants to rely on the specification, it is natural to ask for techniques and tools which can guide and support the work of performing the proof. In general, a correctness proof can never be fully automatized since there are usually different objects to compare: specifications and algebras. The algebra to which a specification is related, however, must be given in some mathematical terminology, since otherwise it is impossible to formulate a correctness proof at all. Since correctness is in general a recursively undecidable predicate it remains the duty of the specifier to perform the correctness proof in most cases. On the other hand, there are usually parts in a correctness proof which allow for an automatization. We have abstained to discuss in this volume the criteria of correctness which can be tested by a theorem prover though much work has been done in this direction. Instead, we have emphasized on the “semantical” conditions for correctness and we will try in this chapter to expose some of the experience in designing specifications and in correctness proofs. This “pragmatic” component of algebraic specification of abstract data types has rarely been discussed in the literature, but is certainly of major importance for the application of algebraic specifications.