Programmverifikation

Korrektheit von If-Else-Anweisungen

 aufwärts

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

{P und B} S1 {Q},  {P und ¬B} S2 {Q}
{Pif(B) S1 else S2 {Q}

 

 

Um also {Pif(B) S1 else S2 {Q} zu beweisen, müssen {P und B} S1 {Q} und {P und ¬B} S2 {Q} bewiesen werden. In Bild 1 sind diese Vor- und Nach­bedingungen in das Fluss­diagramm der If-Else-Anweisung einge­zeichnet.

Bild 1: Vor- und Nachbedingungen bei der If-Else-Anweisung
Bild 1: Vor- und Nachbedingungen bei der If-Else-Anweisung

Beispiel:  Das folgende Programm berechnet das Maximum von zwei Werten a und b, das Ergebnis ist m.

if (a>b)
    m=a;
else
    m=b;

Die Nach­bedingung Q des Programms ist

Q:   m = max(a, b)

 

Wir führen nun zwei getrennte Beweise für die beiden Prämissen, und zwar zunächst   {P und Bm=a; {Q}   und dann   {P und ¬Bm=b; {Q}   mit

B:    a > b

 

Prämisse If1:  If-Teil

Zuerst zeigen wir {P und Bm=a; {Q}.

Der Beweis wird von unten nach oben geführt, unter Benutzung der Wert­zuweisungsregel und der Konsequenz­regel. Es stellt sich heraus, dass Ptrue die schwächste Vorbedingung für diesen Zweig ist.

{ P  und  B }(8)
{ true  und  a > b }(7)
{ a > b }(6)
{ a > b  oder  a = b }(5)
{ agrößer gleichb }(4)
{ a = max(a, b) }(3)
m=a;
{ m = max(a, b) }(2)
{ Q }(1)

Die Konsequenz­regel ermöglicht das Verschärfen von Bedingungen nach oben hin. Beim Übergang von Schritt (5) zu Schritt (6) haben wir davon Gebrauch gemacht und die Bedingung durch Weglassen einer Oder-Bedingung verschärft. Beim Übergang von Schritt (6) zu Schritt (7) haben wir die Bedingung durch Hinzufügen einer Und-Bedingung verschärft 1).

Prämisse If2:  Else-Teil

Als nächstes zeigen wir {P und ¬B} m=b; {Q}.

Auch hier ergibt sich Ptrue als schwächste Vorbedingung.

{ P  und  ¬B }(8)
{ true  und  ¬ a > b }(7)
{ ¬ a > b }(6)
{ akleiner gleichb }(5)
{ bgrößer gleicha }(4)
{ b = max(a, b) }(3)
m=b;
{ m = max(a, b) }(2)
{ Q }(1)

 

Nachdem wir diese beiden Beweise getrennt geführt haben, können wir aufgrund der Schlussregel für die If-Anweisung folgern

{ trueif (a>b) m=a; else m=b;  { m = max (a, b) }

d.h. wir haben bewiesen, dass ohne irgendeine besondere Vorbedingung (außer der Bedingung true, die immer wahr ist) das Programm das Gewünschte tut.

 

Aufgaben

Aufgabe 1:  Folgendes Programm­stück ist gegeben:

if (a>b)
{
    h=a;
    a=b;
    b=h;
}

Geben Sie die schwächste Vorbedingung P für die Nach­bedingung Qakleiner gleichb  an.

Aufgabe 2:  Entwickeln Sie eine vereinfachte Schlussregel für die If-Anweisung ohne Else-Teil.


1)  nur formal, nicht tatsächlich, denn (6) und (7) sind äquivalent

 

Weiter mit:   [Korrektheit von While-Schleifen]   [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