Loading…
Correctness, completeness, and consistency of equational data type specifications
Correctness, completeness, and consistency of equational data type specifications
Padawitz, Peter
Fak. 4 Elektrotechnik und Informatik
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.
Die Methode der schrittweisen Erweiterung von Gleichungs spezifikationen für abstrakte Datentypen erlaubt es, parallel zum Entwurf eines Softwaresystems dessen Korrekt heitsbeweis zu führen: Der Gesamtentwurf ist korrekt, wenn die Semantik der "Basis "-Spezifikation mit dem Modell des Datentyps übereinstimmt und ihre Erweiterung "vollständig" und "konsistent" bezüglich der Basis ist.
Ausgehend von dem von der ADJ-Gruppe geprägten Korrektheitsbegriff für parametrisierte Spezifikationen entwickeln wir auf der Grundlage des Kalküls der Gleichungslogik beweistheoretische Kriterien für Korrektheit, Vollständig keit und Konsistenz. Diese Kriterien werden zunehmend verfeinert, wobei einerseits Normalisierungs- und Konfluenzeigenschaften gleichungsinduzierter Termersetzungen einbezogen werden und andererseits Spezifikationen mit Konditionalen, die auf der aussagenlogischen Semantik Boolescher Ausdrücke aufbauen, gesondert behandelt werden. Die Verfeinerung der Kriterien endet bei entscheidbaren oder zumindest relativ zur Semantik der Basisspezifikation entscheidbaren Bedingungen. Ihre Entscheidbarkeit folgt aus ihrer Charakterisierung durch induktiv definierte Prädikate.
Von zentraler Bedeutung in dieser Hierarchie beweistheoretischer Kriterien sind zunächst das Korrektheitstheorem 1.15 und die Extensionstheoreme 2.8 und 2.10, die wesentliche Charakterisierungen der die Theoreme benennenden Eigenschaften beinhalten. Der Satz 7.7 bzw. - für Spezifikationen mit Konditionalen - 8.5 liefert entscheidbare Vollständigkeitskriterien, die - wie Beispiele belegen werden - noch recht schwach sind. Das Vollständigkeitstheorem 8.16 verbindet syntaktische und semantische Anforderungen an die Spezifikation und findet häufig dann Anwendung, wenn die ausschließlich syntaktischen Bedingungen von 7.7 bzw. 8.5 nicht gelten. Die Sätze 9.18 und 10.15 bzw. - für Spezifikationen mit Konditionalen - 11.10 und 11.11 geben entscheidbare Konsistenzkriterien an, wobei auf 10.15 bzw. 11.11 dann zurückgegriffen werden muß, wenn die Gleichungen der Basisspezifikation nicht normalisierend sind.
