Formale Verifikation - Aufgaben

Aufgabe 1:  Was tut das folgende Programm­stück?

x=x+y;
y=x-y;
x=x-y;

Aufgabe 2:  Beweisen Sie

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

Lösung:  

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

Aufgabe 3:  Gegeben sei folgendes Programm­stück X mit int-Variablen a, b, x, y und r:

x=a;
y=b;
while (y!=0)
{
    r=x%y;
    x=y;
    y=r;
}

Das Programm soll den größten gemeinsamen Teiler von a und b berechnen.

Beweisen Sie die partielle Korrektheit von X bezüglich der Vorbedingung Q:  true und der Nach­bedingung

R:   ggt(a, b) = ggt(x, y)    y = 0.

Aus der Nach­bedingung folgt, dass x der größte gemeinsame Teiler von a und b ist, denn es gilt

ggt(a, b) = ggt(x, y)    y = 0      ggt(a, b) = ggt(x, 0) = x.

Benutzen Sie beim Beweis des Schleifen­körpers, dass

ggt(x, y)  =  ggt(y, x mod y)

gilt, falls y ≠ 0 ist.

Aufgabe 4:  Beweisen Sie die totale Korrektheit des Programm­stücks X aus der vorigen Aufgabe bezüglich der Vorbedingung Q:  b0 und der Nach­bedingung

R:   ggt(a, b) = ggt(x, y)    y = 0.