Deklarative Programmierung eines Generators für Beweisobligationen
Event-B ist eine Notation zur formalen Modellierung computerbasierter Systeme. Zur systematischen Analyse der Modelle dienen Beweisobligationen: Sequenten, die aus Elementen des Modells kombiniert werden.
Beispiel: Ein Modell besteht aus eine Liste von Invarianten I_1, I_2, ..., I_n und einer Liste von Ereignissen der Form (G_k --> x := A_k) für 1 <= k <= m. Dann ist zu beweisen, daß sämtliche Ereignisse alle Invarianten erhalten. Das entspricht den Sequenten:
-
(*) I_1, I_2, ..., I_n, G_k |- I_j[x := A_k]
für 1 <= j <= n, 1 <= k <= m.
Die Beweisobligationen werden durch einen Beweisobligationengenerator (BOG) systematisch aus den Elementen eines Models erzeugt. Der BOG ließt ein Modell ein und gibt eine Sammlung von Beweisobligationen aus. Es gibt viele Möglichkeiten ein BOG zu implementieren, z.B.:
- Als Bestandteil eines Theorembeweisers üblicherweise Heuristikbasiert
- Deklarativ über einen Problemspezifischen Interpreter
- Imperativ (z.B. in Java) mit einem rigiden Ersetzungsschema
Methode 1 ist nicht sehr effizient und das Ergebnis eines Laufes des BOG ist schwer vorherzusehen. Das heißt, ein Benutzer des BOG kann nicht in einfacher Weise die Beweisobligationen mit dem Ausgangsmodell in Beziehung setzen. Methode 3 ist schwer zu warten und an spezielle Kriterien anzupassen. Methode 2 erscheint eine gangbare Alternative:
- Die Beweisobligationen wären einfach zu implementieren.
- Der BOG verhielte sich vorhersagbar.
- Der BOG wäre hinreichend effizient; vergleichbar mit Methode 3.
- Der BOG wäre einfach wartbar.
- Der BOG wäre leicht anpaßbar (auch durch den Benutzer).
Die Implementierung sollte ein Model als einen Datentyp auffassen und Methoden zum Auffinden der Invarianten, Ereignisse, usw enthalten. Darauf aufbauend sollte ein Interpreter implementiert werden, der Beweisobligationen interpretiert und so als BOG dienen kann. Idealerweise würde eine Formel von der Form (*) bereits als Eingabe akzeptiert. Als Implementationssprachen böten sich für diese Problemstellung Prolog oder Haskell an.