Programmverifikation

Korrektheit von While-Schleifen

 aufwärts

Partielle Korrektheit

Die Schlussregel für die While-Schleife ergibt sich aus dem Fluss­diagramm (Bild 1). Sie lautet

P und ¬BfolgtR,   {P und B} S {P}
{Pwhile(B) S {R}

 

Die Schlussregel besagt, dass wenn die Prämissen P und ¬BfolgtR und {P und B} S {P} erfüllt sind, der Schluss {Pwhile(B) S {R} gültig ist. Hierbei gilt die Nach­bedingung R allerdings nur, wie in Bild 1 zu sehen, wenn die Schleife verlassen wird, wenn die Schleife also terminiert. Korrektheit unter dieser Voraus­setzung wird als partielle Korrektheit bezeichnet, im Gegensatz zur totalen Korrektheit.

Bild 1: Vor- und Nachbedingungen bei der While-Schleife
Bild 1: Vor- und Nachbedingungen bei der While-Schleife

Die Bedingung P in Bild 1 ist die Schleifen­invariante. Der Begriff Invariante bedeutet, dass die Bedingung vor und nach der Schleife unverändert bleibt.

Beispiel:  Das folgende Programm­stück berechnet  n! = 1 · 2 · 3 · ... · n.

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

 

Das Ergebnis n! soll am Ende des Programms als Wert der Variablen f erscheinen. Die Nach­bedingung des Programms lautet also

R:   f = n!

Der Beweis des Programms wird von unten nach oben geführt. Wir bezeichnen das gesamte Programm mit X, die While-Schleife mit W und den Schleifen­körper mit S. Zuerst wird die While-Schleife W bewiesen.

 

Beweis der While-Schleife W

Für den Beweis der While-Schleife beweisen wir die beiden Prämissen der Schlussregel.

Prämisse While1:  Nach­bedingung R in die Form P und ¬B bringen

Wir bringen die Nach­bedingung R, die am Ende der While-Schleife gilt, in die Form P und ¬B. Hierzu ist es erforderlich, in irgendeiner Weise die Bedingung ¬B:  igrößer gleichn und damit die Variable i einzuführen.

{ P  und  ¬B }(5)
{ f = i!  und  ikleiner gleichn  und  igrößer gleichn }(4)
{ f = i!  und  i = n }(3)
{ f = n! }(2)
{ R }(1)

 

Aus (4) ergibt sich somit die Schleifen­invariante P, die wir benötigen, um die zweite Prämisse zu beweisen.

 P:   f = i!  und  ikleiner gleichn

 

Prämisse While2:  Beweis des Schleifen­körpers S

Wir beweisen nun {P und B} S {P} für den Schleifen­körper S.

 

Der Beweis wird von unten nach oben geführt:

{ P  und  B }(7)
{ f = i!  und  ikleiner gleichn  und  i < n }(6)
{ f = i!  und  i < n }(5)
{ f·(i+1) = (i+1)!  und  i+1kleiner gleichn }(4)
i=i+1;
{ f·i = i!  und  ikleiner gleichn }(3)
f=f*i;
{ f = i!  und  ikleiner gleichn }(2)
{ P }(1)

Hierbei gilt (5) folgt (4), da aus f = i! durch Multi­plikation mit i+1 folgt f·(i+1) = (i+1)! und aus i < n folgt i+1kleiner gleichn. Ferner gilt (6) folgt (5), da (6) eine Verschärfung von (5) ist.

 

Da die beiden Prämissen erfüllt sind, gilt somit aufgrund der Schlussregel für die While-Schleife W folgende Korrektheits­formel:

{ f = i!  und  ikleiner gleichn } W { f = n! }.

 

Beweis des gesamten Programms X

Der Rest des Programms wird wie folgt bewiesen:

{ Q }(7)
{ ngrößer gleich0 }(6)
{ true  und  0kleiner gleichn }(5)
{ 1 = 0!  und  0kleiner gleichn }(4)
i=0;
{ 1 = i!  und  ikleiner gleichn }(3)
f=1;
{ f = i!  und  ikleiner gleichn }(2)
{ P }(1)

 

Als schwächste Vorbedingung ergibt sich ngrößer gleich0. Insgesamt gilt also für das gesamte Programm X

{ ngrößer gleich0 }
X
{ f = n! }

Aufgaben

Aufgabe 1:  (Rest bei ganzzahliger Division)

Gegeben sei folgendes Programm X mit ganzzahligen Variablen a, b, q und r:

q=0;
r=a;
while (r>=b)
{
    q=q+1;
    r=r-b;
}

Das Programm soll den Rest r bei ganzzahliger Division von a durch b berechnen.

Beweisen Sie, dass die Nach­bedingung

R:   a = q·b + r  und  rgrößer gleich0  und  r < b

gilt, falls die Schleife terminiert (partielle Korrektheit).

Wie lautet die Schleifen­invariante P? Welches ist die schwächste Vorbedingung Q des Programms?

Aufgabe 2:  (Berechnung von n2 mithilfe von Additionen)

Meistens gelingt es, beim Beweis der Prämisse While1 die Schleifen­invariante P zu finden. Bei folgendem Programm ergibt sich P auf diese Weise nicht automatisch.

Gegeben sei folgendes Programm X:

k=-1;
i=0;
q=0;
while (i<n)
{
    i=i+1;
    k=k+2;
    q=q+k;
}

Das Programm X berechnet das Quadrat einer ganzen Zahl n.

 

Ermitteln Sie die schwächste Vorbedingung Q für die Korrektheits­formel {Q} X {R} mit der Nach­bedingung

R:   q = n2

 

Aufgabe 3:  Entwickeln Sie eine Schlussregel für die Do-While-Schleife  do S while (B);. Welche Prämissen sind für die Schlussregel erforderlich, damit als Konklusion {Q} do S while (B); {R} gilt?

Hinweis: Zeichnen Sie das Fluss­diagramm einer Do-While-Schleife und tragen Sie die jeweils geltenden Bedingungen in das Fluss­diagramm ein. Vergleichen Sie diese Bedingungen mit den ent­sprechenden Bedingungen im Fluss­diagramm für das äquivalente Programm­stück  S; while (BS.

 

Weiter mit:   [Totale Korrektheit]   [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