Programmverifikation

Totale Korrektheit von While-Schleifen

 aufwärts

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

P und ¬BfolgtR,   {P und B} S {P}
{Pwhile(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 und B folgt (Bild 1):

P und B folgt 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 und Bz=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 und ¬BfolgtR,   {P und B} S {P},   P und BfolgtE > 0,   {P und Bz=E; S {E < z}
{Pwhile (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

En-i,

dass

P und B folgt E > 0

gilt, denn mit  Bi < n  ergibt sich sofort

P und B  folgt  B  folgt  n > i  folgt  n-i > 0.

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

Es ist zu zeigen:

{P und Bz=E; S {E < z}.

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

{ P und 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 Ptrue.

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:

Pigrößer gleich0

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

Prämissen While1 und While2:  Partielle Korrektheit

Offenbar ist {igrößer gleich0} W {i = 0} im Sinne der partiellen Korrektheit erfüllt.

Prämisse While3:  Ganzzahliger Ausdruck E > 0

Mit dem Ausdruck

Ei

gilt offenbar

P und B folgt E > 0,

denn mit  Pigrößer gleich0 und Bi ≠ 0 sowie Ei ergibt sich

P und B  folgt  igrößer gleich0  und  i ≠ 0  folgt  i > 0  folgt  E > 0.

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

Es ist zu zeigen:

{P und Bz=E; S {E < z}.

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

{ P und 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 Pigrößer gleich0 und der Nach­bedingung Qi = 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 Ptrue.

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 und B folgt E > 0.

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

Ferner ist zu zeigen:

{P und Bz=E; S {E < z}.

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

{ P und 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 und B abgeleitet werden kann.

 

Weiter mit:   [Halteproblem]   [Literatur]  oder   up

 

homeH.W. Lang   Hochschule Flensburg   lang@hs-flensburg.de   Impressum   ©  
Valid HTML 4.01 Transitional

Hochschule Flensburg
Campus Flensburg

Informatik in Flensburg studieren...

 

Neu gestaltetes Studienangebot:

Bachelor-Studiengang
Angewandte Informatik

mit Schwerpunkten auf den Themen Software, Web, Mobile, Security und Usability.

Ihr Abschluss
nach 7 Semestern:
Bachelor of Science

 

Ebenfalls ganz neu:

Master-Studiengang
Angewandte Informatik

Ein projektorientiertes Studium auf höchstem Niveau mit den Schwerpunkten Internet-Sicherheit, Mobile Computing und Human-Computer Interaction.

Ihr Abschluss
nach 3 Semestern:
Master of Science

 

Weitere Informatik-Studienangebote an der Hochschule Flensburg:

Medieninformatik

Wirtschaftsinformatik