Programmverifikation

Totale Korrektheit von While-Schleifen

Als Schlussregel für die While-Schleife hatten wir bisher kennen gelernt:

P ∧ ¬B ⇒ R,   {P ∧ B} S {P}
{P} while(B) S {R}

 

Hierbei gilt die Nach­bedingung R allerdings nur, wenn die Schleife verlassen wird, wenn sie also terminiert. Korrektheit unter dieser Voraus­setzung wird als partielle Korrektheit bezeichnet.

Im Folgenden geht es darum, zusätzliche Bedingungen dafür zu finden, dass die Schleife auch terminiert.

Totale Korrektheit

Definition:  Ein Programm S wird als partiell korrekt bezüglich einer Vorbedingung P und einer Nach­bedingung Q bezeichnet, wenn es die Korrektheits­formel {P} S {Q} erfüllt, falls es terminiert. Als total korrekt wird es bezeichnet, wenn es die Korrektheits­formel {P} S {Q} erfüllt und terminiert.

Bedingungen für die Terminierung

Um zu beweisen, dass eine While-Schleife terminiert, sucht man nach einem ganzzahligen Ausdruck E, der

Gibt es einen solchen ganzzahligen Ausdruck E, so kann die Schleife nicht unendlich oft durchlaufen werden, sondern muss irgendwann abbrechen.

Die Tatsache, dass der Ausdruck E vor Ausführung des Schleifen­körpers positiv ist, ist immer dann gegeben, wenn E > 0 aus P ∧ B folgt (Bild 1):

P ∧ B  ⇒  E > 0.

Die Tatsache, dass der Ausdruck E beim Durchlauf durch den Schleifen­körper S vermindert wird, wenn dieser betreten wird, lässt sich so ausdrücken:

{P ∧ B} z=E; S {E < z}.

Hierbei ist z=E; eine zusätzliche Anweisung vor dem Schleifen­körper S und z eine neue Variable, die sonst nirgendwo vorkommt. Sie nimmt den Wert des ganzzahligen Ausdrucks E vor Ausführung von S auf. Nach Ausführung von S muss E kleiner als z sein, also in S vermindert worden sein.

 

Bild 1: Ein ganzzahliger Ausdruck E wird im Schleifenkörper S vermindert 

Bild 1: Ein ganzzahliger Ausdruck E wird im Schleifenkörper S vermindert

 

Schlussregel für die totale Korrektheit

Die Schlussregel für den Beweis der totalen Korrektheit der While-Schleife enthält die beiden Prämissen der Schlussregel für die partielle Korrektheit sowie zwei weitere Prämissen; sie lautet somit:

P ∧ ¬B ⇒ R,   {P ∧ B} S {P},   P ∧ B ⇒ E > 0,   {P ∧ B} z=E; S {E < z}
{P} while (B) S {R}

 

Um die totale Korrektheit einer While-Schleife zu beweisen, müssen also vier Prämissen bewiesen werden: 1.+2. die beiden Prämissen für die partielle Korrektheit, 3. die Tatsache, dass der ganzzahlige Ausdruck E vor Durchlaufen des Schleifen­körpers positiv ist und 4. die Tatsache, dass E beim Durchlaufen des Schleifen­körpers vermindert wird.

In den folgenden Beispielen werden diese vier Prämissen jeweils einzeln bewiesen. Wir bezeichnen diese vier Prämissen mit While1, ..., While4.

Beispiel

Beispiel:  Wir betrachten die While-Schleife W mit Schleifen­körper S aus dem Programm zur Berechnung von n! :

while (i<n)
{
    i=i+1;
    f=f*i;
}

 

Prämissen While1 und While2:  Partielle Korrektheit

Wir hatten die partielle Korrektheit bereits gezeigt.

Prämisse While3:  Ganzzahliger Ausdruck E > 0

Für den Beweis der totalen Korrektheit benötigen wir einen ganzzahligen Ausdruck E, der beim Eintritt in den Schleifen­körper positiv ist und im Schleifen­körper vermindert wird. Die ganzzahlige Variable i wird dort um 1 vermehrt, also wird der Ausdruck n-i vermindert.

Tatsächlich gilt mit

E:  n-i,

dass

P ∧ B  ⇒  E > 0

gilt, denn mit  B: i < n  ergibt sich sofort

P ∧ B  ⇒  B  ⇒  n > i  ⇒  n-i > 0.

Prämisse While4:  Ausdruck E wird im Schleifen­körper vermindert

Es ist zu zeigen:

{P ∧ B} z=E; S {E < z}.

Mit  E: n-i  lässt sich der Beweis wie folgt führen:

{ P ∧ B }(9)
{ true }(8)
{ -1 < 0 }(7)
{ n-i-1 < n-i }(6)
z=n-i;
{ n-i-1 < z }(5)
{ n-(i+1) < z }(4)
i=i+1;
{ n-i < z }(3)
f=f*i;
{ n-i < z }(2)
{ E < z }(1)

Damit ist insgesamt die totale Korrektheit der While-Schleife W gezeigt.

Die Schleifen­invariante P ist beim Beweis der Terminierung hier gar nicht eingegangen. Dies ist jedoch nicht immer so; im Allgemeinen lässt sich die Terminierung nur im Zusammenhang mit einer geeigneten Bedingung P zeigen. Dies wird in dem nächsten Beispiel deutlich.

Beispiel: Schärfere Vorbedingung

Oft ist für den Beweis der totalen Korrektheit einer While-Schleife eine schärfere Vorbedingung P erforderlich als für den Beweis der partiellen Korrektheit.

Schärfere Vorbedingung für Terminierung

In folgendem Beispiel wird eine bestimmte Vorbedingung P eigens für den Zweck eingeführt, um die Terminierung der Schleife beweisen zu können.

Beispiel:  Wir betrachten folgende While-Schleife W mit Schleifen­körper S:

while (i!=0)
    i=i-1;

 

Offenbar gilt {true} W {i = 0} im Sinne der partiellen Korrektheit, mit P: true.

Für den Beweis der totalen Korrektheit benötigen wir einen ganzzahligen Ausdruck E, der im Schleifen­körper vermindert wird und der vor dem Eintritt in den Schleifen­körper stets positiv ist. Weder aus P noch aus B lässt sich hier jedoch ein solcher Ausdruck ableiten.

Tatsächlich terminiert die Schleife auch nicht, wenn i zu Beginn negativ ist. Wir müssen also gewähr­leisten, dass i zu Beginn nicht negativ ist, indem wir eine schärfere Vorbedingung P verwenden:

P:  i ≥ 0

Mit dieser neuen Bedingung P beweisen wir zunächst die partielle Korrektheit.

Prämissen While1 und While2:  Partielle Korrektheit

Offenbar ist {i ≥ 0} W {i = 0} im Sinne der partiellen Korrektheit erfüllt.

Prämisse While3:  Ganzzahliger Ausdruck E > 0

Mit dem Ausdruck

E: i

gilt offenbar

P ∧ B  ⇒  E > 0,

denn mit  P: i ≥ 0 und B: i ≠ 0 sowie E: i ergibt sich

P ∧ B  ⇒  i ≥ 0  ∧  i ≠ 0  ⇒  i > 0  ⇒  E > 0.

Prämisse While4:  Ausdruck E wird im Schleifen­körper vermindert

Es ist zu zeigen:

{P ∧ B} z=E; S {E < z}.

Mit  E: i  lässt sich der Beweis wie folgt führen:

{ P ∧ B }(7)
{ true }(6)
{ 0 < 1 }(5)
{ i-1 < i }(4)
z=i;
{ i-1 < z }(3)
i=i-1;
{ i < z }(2)
{ E < z }(1)

Damit ist insgesamt die totale Korrektheit der While-Schleife W bezüglich der Vorbedingung P: i ≥ 0 und der Nach­bedingung Q: i = 0 gezeigt.

Beispiel: Triviale While-Schleife

Die Aussagekraft der Schlussregel für die totale Korrektheit wird deutlich, wenn es gelingt, auch triviale While-Schleifen damit zu beweisen. Hierzu dient das folgende Beispiel.

Beispiel:  Wir betrachten folgende While-Schleife W mit leerem Schleifen­körper S:

while (false) ;

 

Prämissen While1 und While2:  Partielle Korrektheit

Offenbar gilt {true} W {true} im Sinne der partiellen Korrektheit, mit P: true.

Prämisse While3:  Ganzzahliger Ausdruck E > 0

Für den Beweis der totalen Korrektheit benötigen wir einen ganzzahligen Ausdruck E, der vor Eintritt in den Schleifen­körper positiv ist und im Schleifen­körper vermindert wird. Da der Schleifen­körper leer ist, kann eigentlich dort nichts vermindert werden. Wir versuchen den Beweis trotzdem mit dem Ausdruck

E: 1

Offenbar gilt

P ∧ B  ⇒  E > 0.

Prämisse While4:  Ausdruck E wird im Schleifen­körper vermindert

Ferner ist zu zeigen:

{P ∧ B} z=E; S {E < z}.

Mit  E: 1  lässt sich der Beweis wie folgt führen:

{ P ∧ B }(6)
{ B }(5)
{ false }(4)
{ 1 < 1 }(3)
z=1;
{ 1 < z }(2)
{ E < z }(1)

Damit ist insgesamt die totale Korrektheit der While-Schleife W gezeigt.

Aufgaben

Aufgabe 1:  Beweisen Sie die totale Korrektheit des Programms zur Berechnung des Rests bei ganzzahliger Division (siehe Aufgabe).

Hinweis: Für den Beweis der totalen Korrektheit muss die Schleifen­invariante P verschärft werden, damit es einen ganzzahligen Ausdruck E gibt, der im Schleifen­körper vermindert wird und für den E > 0 aus P ∧ B abgeleitet werden kann.

 

Weiter mit:   [Halteproblem]   [Literatur]  oder   [up]

 

H.W. Lang   mail@hwlang.de   Impressum   Datenschutz
Diese Webseiten sind während meiner Lehrtätigkeit an der Hochschule Flensburg entstanden