Projekt: Spezifikation und Verifikation im Rahmen der Typtheorie

Laufzeit: seit 1996

Schlagworte: Typ-Theorie, Logik höherer Ordnung, Verifikation, Spezifikation, Nebenläufige Systeme/Algorithmen, Temporale Logik, Petri-Netze, UNITY

Bemerkungen zur Typtheorie

Eine Logik partieller Funktionen basierend auf einfacher Typ-Theorie (simply typed lambda calculus, Church 1940) wurde bereits bei der Untersuchung zyklischer Ordnungen in Form des Werkzeugs IMPS (interactive mathematical proof system) eingesetzt.

Moderne Typ-Theorien wie z.B. ECC (extended calculus of constructions, oder (CIC) (calculus of inductive constructions) sind im wesentlichen funktionale Programmiersprachen mit extrem ausdrucksstarken Typen. Eine Typ-Theorie wird definiert durch ein formales System, daß es gestattet Typisierungen der Form A:B abzuleiten. Letzteres ist so zu interpretieren, daß A ein Element vom Typ B ist. Wünschenswerterweise (wie bei ECC und CIC) ist die Ableitbarkeit einer Typisierung entscheidbar. Die Möglichkeiten, Typen und deren Elemente zu bilden, sind vielfältig. Zusätzlich zu (verallgemeinerten) Funktionstypen und Produkttypen ist es möglich Typen induktiv zu definieren.

Intuitionistische Logik höherer Ordnung laßt sich in diesen Typ-Theorien entsprechend der Propositions-as-Types-Interpretation einbetten. Eine Proposition wird dabei durch einen Typ repräsentiert, dessen Elemente genau die Beweise der Proposition sind. Der Beweis einer Implikation A => B ist beispielsweise ein Element vom Typ A -> B, d.h. eine totale Funktion, die einen Beweis für A in einen Beweis für B überführt. Das Beweisen dieser Implikation entspricht der Konstruktion einer solchen Funktion. Die Entscheidbarkeit des Typechecking impliziert damit die Entscheidbarkeit des Proofchecking.

Der konstruktive Beweis einer Existenzaussage kann nicht durch Widerspruch geführt werden, sondern benötigt explizit ein Element (witness) mit den geforderten Eigenschaften. Ist S eine Existenzaussage der Form ''für alle x in A existiert ein y in B mit PHI(x,y)'', ist der Beweis ein Element dieses Typs, d.h. eine Funktion, die für ein x in A ein y in B liefert so daß PHI(x,y) gilt. Diese Funktion ist entspricht einem funktionalen Programm P, also einer Implementierung der Spezifikation S, kurz P:S.

Ziele:

Das Ziel dieses Projekts ist es, zunächst eine Bibliothek allgemeiner mathematischer Grundbegriffe in Typ-Theorie aufzubauen bzw. existierende Bibliotheken zu erweitern. Darauf aufbauend soll eine universelle Bibliothek zur Spezifikation und Verifikation nebenläufiger Systeme entstehen, die anhand von Fallstudien erprobt, erweitert und verbessert wird.

Bei dem Entwurf sollen insbesondere die Aspekte der Modularisierung und Kompositionalität sowie die Erfahrungen mit Formalismen wie Temporalen Logiken, (gefärbten) Petri-Netzen und UNITY berücksichtigt werden. Der funktionale Aspekt (wie bei gefärbten Petri-Netzen oder UNITY) wird durch Typ-Theorie auf natürliche Weise unterstützt. Es wird angestrebt den typtheoretischen Spezifikationsbegriff auch auf nicht-funktionale, d.h. reaktive Systeme anzuwenden.

Der Vorteil einer strengen Formalisierung in einer Sprache wie der Typ-Theorie ist die Möglichkeit, mathematische Theorien mit Rechnerunterstützung zu entwickeln und ein hohes Maß an Sicherheit zu erreichen. Konkret werden die Typ-Theorien ECC und CIC durch die Werkzeuge LEGO und COQ implementiert, die in diesem Projekt intensiv verwendet werden.

Publikationen:

• Mark-Oliver Stehr: Embedding UNITY into the Calculus of Inductive Constructions , Fachbereichsbericht FBI-HH-B-214/98, Universität Hamburg, Fachbereich Informatik, September 1998.