Please use this identifier to cite or link to this item: http://dx.doi.org/10.14279/depositonce-5437
Main Title: Correctness, completeness, and consistency of equational data type specifications
Author(s): Padawitz, Peter
Referee(s): Ehrig, Hartmut
Siefkes, Dirk
Granting Institution: Technische Universität Berlin
Type: Doctoral Thesis
Language Code: en
Abstract: 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.
URI: http://depositonce.tu-berlin.de/handle/11303/5835
http://dx.doi.org/10.14279/depositonce-5437
Exam Date: 13-May-1983
Issue Date: 1983
Date Available: 17-Aug-2016
DDC Class: DDC::000 Informatik, Informationswissenschaft, allgemeine Werke::000 Informatik, Wissen, Systeme::004 Datenverarbeitung; Informatik
Subject(s): software
semantics
mathematical proof
equational logic
Softwaresysteme
Semantik
mathematischer Beweis
Gleichungslogik
Creative Commons License: https://creativecommons.org/licenses/by/4.0/
Appears in Collections:Fakultät 4 Elektrotechnik und Informatik » Publications

Files in This Item:
File Description SizeFormat 
padawitz_peter_1983.pdf220.08 MBAdobe PDFThumbnail
View/Open


This item is licensed under a Creative Commons License Creative Commons