Programmverifikation

Semantikregeln

 aufwärts

Wenn wir programmieren, wissen wir ungefähr, wie Programm­anweisungen auszusehen haben, und wir haben auch eine Vorstellung davon, was sie bewirken. Tatsächlich jedoch gibt es formale Regeln, die sowohl die Struktur als auch die Bedeutung von Programm­anweisungen exakt festlegen.

Definition:  Die  Syntax   einer Programmier­sprache ist die Gesamtheit der Regeln, die angeben, was ein Programm ist.

Definition:  Die Semantik einer Programmier­sprache ist die Gesamtheit der Regeln, die angeben, was ein Programm tut.

Die Syntax der Programmier­sprache bestimmt also, welche Zeichen­reihen vom Computer als gültiges Programm angesehen werden. Formal werden die Syntaxregeln im wesentlichen durch eine Grammatik angegeben.

Die Semantik der Programmier­sprache bestimmt, was der Computer macht, wenn er ein Programm ausführt. Formal werden die Semantik­regeln beispiels­weise durch die im Folgenden angegebenen Korrektheits­formeln (Hoare-Tripel – nach C.A.R. Hoarezur Person) und darauf aufbauende Schluss­regeln definiert [Hoa 69].

Korrektheitsformeln

Die Semantik einer Programmier­sprache wie Java enthält Regeln darüber, wie Ausdrücke ausgewertet werden, wie Anweisungen ausgeführt werden, wie Funktions­aufrufe behandelt werden und welche Auswirkungen die Deklaration von Variablen, Typen und Funktionen hat.

Wir beschränken uns auf die Semantik der grund­legenden Anweisungen. Die ent­sprechenden Semantik­regeln werden im Folgenden definiert. Eine solche Regel ist entweder eine Korrektheits­formel der Form {P} S {Q} oder eine Schlussregel.

Definition:  Die Korrektheits­formel {P} S {Q} ist wie folgt zu inter­pretieren: Wenn die Vorbedingung P vor Ausführung der Anweisung S gilt, so gilt nach der Ausführung der Anweisung S die Nach­bedingung Q.

Die Bedingungen P und Q sind logische Formeln. Die Anweisung S kann auch eine zusammen­gesetzte Anweisung sein, z.B. eine strukturierte Anweisung wie eine Schleife oder ein Block von mehreren Anweisungen.

Die Schluss­regeln sind Vorschriften, die angeben, wie aus vorhandenen Korrektheits­formeln oder logischen Formeln neue Korrektheits­formeln gebildet werden können. Die Schreibweise ist folgende:

A1, ..., Ak
B

Die Bedeutung einer solchen Schlussregel ist: Wenn A1, ..., Ak logische Formeln oder Korrektheits­formeln sind, so ist auch B eine Korrektheits­formel. Die über dem Strich stehenden Formeln heißen Prämissen, die unter dem Strich stehende Formel heißt Konklusion.

Es folgen die Semantik­regeln für einige grundlegende Anweisungen der Programmier­sprache Java; diese werden in den darauf folgenden Abschnitten erläutert.

 

Regeln
{P[xPfeil nach linkse]} x=e; {P} (Wert­zuweisungsaxiom)
  
{P} S1 {Q},  {Q} S2 {R}
{P} S1 S2 {R}
 (Kompositions­regel)
  
PfolgtQ
{P} {Q}
 (Konsequenz­regel / leere Anweisung)
  
{P und B} S1 {Q},  {P und ¬B} S2 {Q}
{Pif (B) S1 else S2 {Q}
 (If-Else-Regel)
  
P und ¬BfolgtR,   {P und B} S {P}
{Pwhile(B) S {R}
 (While-Regel)
  
Wertzuweisungsaxiom

Von grund­legender Bedeutung ist die Regel für die Wert­zuweisung. Sie gibt die schwächste Vorbedingung an, die vor der Zuweisung x=e; gilt, wenn als Nach­bedingung P gilt. Hierbei ergibt sich die Vorbedingung P[xPfeil nach linkse], indem in der Nach­bedingung P alle freien Vorkommen der Variablen x durch den Ausdruck e ersetzt werden.

Beispiel:  Es gilt

{ x+1 = 3 } x=x+1; { x = 3 }

In der Nach­bedingung Px = 3 kommt x als freie Variable vor. Wird in P die Variable x durch den Ausdruck x+1 ersetzt, so ergibt sich die Vorbedingung x+1 = 3.

Diese Bedingung lässt sich durch die äquivalente Bedingung x = 2 ersetzen – formal werden hierfür jedoch die Kompositions­regel und die Konsequenz­regel benötigt (siehe Beispiel weiter unten).

Da die Vorbedingung sich aus der Nach­bedingung ergibt, werden Programme "von unten nach oben" bewiesen. Der fertige Beweis wird dann von oben nach unten gelesen.

Kompositionsregel

Die Regel für die Komposition, also für die Hinter­einanderausführung von Anweisungen, wird gebraucht, um einen Beweis für ein Programm Schritt für Schritt führen zu können. Zwischen je zwei Anweisungen steht eine Bedingung Q, die Nach­bedingung der einen und zugleich Vorbedingung der anderen Anweisung ist. Eine solche Bedingung, die in geschweiften Klammern an bestimmter Stelle im Programm steht, wird als Zusicherung (engl.: assertion) bezeichnet.

Beispiel:  In folgendem Programm werden die Werte der Variablen a und b vertauscht. Der Beweis wird von unten nach oben geführt. Es wird dreimal das Wert­zuweisungsaxiom angewendet. Als erstes werden in der Zusicherung (1) alle (freien) Vorkommen der Variablen b, die auf der linken Seite der Wert­zuweisung b=h; steht, durch die rechte Seite h ersetzt. Das Ergebnis ist die Zusicherung (2). Dann werden in (2) alle Vorkommen von a durch b ersetzt, und schließlich in (3) alle Vorkommen von h durch a.

{ b = A  und  a = B }(4)
h=a;
{ b = A  und  h = B }(3)
a=b;
{ a = A  und  h = B }(2)
b=h;
{ a = A  und  b = B }(1)

 

Insgesamt gilt also

{ b = A  und  a = B } h=a; a=b; b=h; { a = A  und  b = B },

d.h. wenn vor Ausführung des Programms die Variable b den Wert A und die Variable a den Wert B hat, dann hat nach Ausführung des Programms a den Wert A und b den Wert B. Die Werte werden also vertauscht.

 

Konsequenzregel

Die Konsequenz­regel besagt Folgendes: Falls Q Nach­bedingung der leeren Anweisung ist, so ist jede Bedingung P als Vorbedingung gültig, für die gilt PfolgtQ. Die Konsequenz­regel erlaubt es also, in Verbindung mit der Kompositions­regel, im Beweis eines Programms Bedingungen nach oben hin zu verschärfen. Insbesondere erlaubt sie auch, Bedingungen durch äquivalente Bedingungen zu ersetzen.

Beispiel:  Zu zeigen ist

{ x > 0 } x=x+1; { x > 0 }

Der Beweis wird von unten nach oben geführt.

{ x > 0 }(3)
{ x+1 > 0 }(2)
x=x+1;
{ x > 0 }(1)

Der Übergang zwischen Bedingung (2) und Bedingung (3) ergibt sich aufgrund der Konsequenz­regel, denn es gilt

x > 0  folgt  x+1 > 0

Zwischen (2) und (3) steht eine leere Anweisung.

Bemerkung:  Da wir den Beweis von unten nach oben führen, ergeben sich die Bedingungen, die wir mithilfe der Konsequenz­regel entwickeln, entgegen der Richtung unseres gewohnten logischen Schließens. Wir argumentieren gewisser­maßen in Gegen­richtung des folgt-Pfeils. Dies ist zunächst gewöhnungs­bedürftig und manchmal auch fehler­trächtig.

Bei äquivalenten Umformungen, wie in dem folgenden Beispiel, haben wir kein Problem. Ansonsten aber hilft es, wenn wir uns merken, dass wir Bedingungen nach oben hin verschärfen dürfen.

Insbesondere werden wir häufig Bedingungen dadurch verschärfen, dass wir Und-Bedingungen hinzufügen oder Oder-Bedingungen weglassen.

Beispiel:  Zu beweisen ist die Korrektheits­formel aus dem Beispiel zum Wert­zuweisungsaxiom:

{ x = 2 } x=x+1; { x = 3 }

Der Beweis wird von unten nach oben geführt.

{ x = 2 }(3)
{ x+1 = 3 }(2)
x=x+1;
{ x = 3 }(1)

Der Übergang zwischen Bedingung (2) und Bedingung (3) ergibt sich aufgrund der Konsequenz­regel, denn es gilt

x = 2  genau dann wenn  x+1 = 3

Zwischen (2) und (3) steht eine leere Anweisung.

 

Die Schluss­regeln für die If-Else-Anweisung und für die While-Schleife werden auf den folgenden Seiten erläutert.

Aufgaben

Aufgabe 1:  Beweisen Sie

{ x < y }
x=y-x;
x=y+x;
{ y < x }

 

 

Weiter mit:   [Korrektheit von If-Else-Anweisungen]   [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