1 Charakterisierung der Schnittstelle
Die Schnittstelle entspricht dem Typus "Informationsweitergabe bei sequentieller Abfolge". Die Methodenkategorie PVER dient dem Nachweis, daß ein Programm eine Implementierung einer formalen Spezifikation ist. Eingang für PVER ist also eine formale Spezifikation und je nach ausgewählter Methode von PVER eventuell ein Programm (bei "klassischer Programmverifikation" und "Verifikation while Development"). Abhängig von der ausgewählten Methode aus PVER ist das Ergebnis das Programm (bei "formaler Transformation") oder das Prüfungsergebnis.
Die Methode FS dient also der Beschreibung des Systems, die Methode PVER dagegen wird für den Nachweis eingesetzt, daß die Implementierung konsistent zur formalen Spezifikation ist.
2 Beispiel
Das folgende Programm soll den ganzzahligen Teil der Quadratwurzel einer natürlichen Zahl berechnen. Das Ergebnis wird nach a geschrieben.
Das Programm hat also folgende Vor- und Nachbedingungen (Spezifikation):
Vorbedingung: n ³ 0
Nachbedingung: a=trunc(Wurzel_aus(2,n))
Das PASCAL-ähnliche Programm sei (mit griechischen Buchstaben sind die für den Beweis wichtigen Stellen im Programm markiert):
Die Methode PVER soll nun die partielle Korrektheit des Programms beweisen (falls das Programm terminiert, erfüllt das Ergebnis die Spezifikation) und die Terminiertheit des Programms (das Programm endet nach endlicher Zeit):
Partielle Korrektheit
Zu Beginn der Schleife (bei a :) hat die Variable a den Wert 0, b den Wert 1und c den Wert 1.
Um die Whileschleife zu beweisen, wird eine Invariante gesucht, d. h. eine Eigenschaft, die zu Beginn jeden Schleifendurchgangs (bei b :) gültig ist.
Die Idee der Invariante ist:
Gilt die Invariante zu Beginn des Schleifenrumpfes, so gilt sie auch danach (die Werte der Varianten vor Schleifendurchgang seien mit ' markiert, z. B. a' für den Wert der Variablen a).
Nach Schleifendurchgang gilt:
Hieraus folgt offensichtlich, daß die Invariante auch nach einem Schleifendurchgang gilt. Mit dem Induktionsgesetzt folgt, daß diese vor jedem Schleifendurchgang gilt. Mit der Schleifenabbruchsbedingung und, da a bei jedem Schleifendurchgang um 1 erhöht wird, folgt die Behauptung.
Abbildung 4.17: Hilfsmittel zur Erstellung eines korrekten Programms
Terminiertheit
Die Terminiertheit kann über c bewiesen werden: c ist immer eine natürliche Zahl und wird bei jedem Schleifendurchgang echt größer (siehe Invariante). D. h. spätestens nach (n+1) Schleifendurchgängen muß das Programm abbrechen, da die Abbruchbedingung c > n ist.
3 Werkzeugunterstützung
Aufgrund der Komplexität der Methode PVER ist eine Werkzeugunterstützung unbedingt notwendig. Der Beweiser (bzw. die verwendeten Regeln) muß an die ausgewählte Spezifikationssprache und Programmiersprache angepaßt sein.
Literatur
/ Baader, 90 / Grundlagen der formalen Methoden und Bestandsaufnahme von Werkzeugen und Konzepten
/ Brix, 86 / Grundlagen der "Programmverfikation while Development" werden hier am Beispiel des Siemens Verifikationstools CARTESIANA aufgeführt
/ Kersten, 90 / Mehrere Beiträge zum Thema "Formale Spezifikation und Verifikation"
/ Kröger, 87 / Behandelt temporale Logik und Verifikation von Aussagen in temporärer Logik.
/ Loeckx, 87 / Beschreibt den mathematischen Hintergrund zu verschiedenen formalen Verifikationsmethoden (z. B. Floyd-Methode, axiomatische Methode von Hoare, Fixpunktinduktion), aufgezeigt an mehreren Beispielen. Diskutiert werden auch Probleme der Korrektheit und Vollständigkeit.