Correctness, completeness, and consistency of equational data type specifications
Peter Padawitz · OpenGrey (Institut de l'Information Scientifique et Technique) · 1983
The method of the stepwise extension of equational specifications for abstract data types allows us to prove the correctness of a software system specification in parallel to its stepwise design. The whole specification is correct if the semantics of the "base" specification agrees with the data type model and if its extension is "complete" and "consistent" with respect to the basis. Starting from the correctness notion for parameterized specifications, which was introduced by the ADJ group, we develop proof-theoretical criteria for correctness, completeness and consistency that originate in the calculus of equational logic. These criteria will be refined more and more: On one hand normalization and confluence properties will be included; on the other hand specifications with conditionals, which presume that Boolean expressions are interpreted as in propositional logic, will be treated seperately. At the end the refinement yields conditions, which are decidable or at least decidable relative to the semantics of the base specification. Their decidability results from their characterization by inductively defined predicates. The hierarchy of proof-theoretical criteria starts with Correctness Thm. 1.15 and Extension Thms. 2.8 and 2.10, which present the main characterizations of the properties that name these theorems. Thm. 7.7 and - for specifications with conditionals - 8.5 yields decidable but rather weak completeness criteria. Completeness Thm. 8.16 combines syntactical and semantical requirements to the specifications and is used when the exclusively syntactical conditions of 7.7 or 8.5 do not hold. Thms. 9.18 and 10.15 as also - for specifications with conditionals - 11.10 and 11.11 state decidable consistency criteria. 10.15 and 11.10 must be referred to whenever the equations of the base specification are not normalizing.