Formale Verifikation - Aufgaben

Bitlänge einer Zahl

Gesucht ist die Länge n der Binärdarstellung einer natürlichen Zahl a. So hat beispielsweise die Zahl a = 13 die Binärdarstellung 1101, denn 13 = 1·8 + 1·4 + 0·2 + 1·1. Die Binärdarstellung der Zahl 13 beansprucht 4 Ziffern, die Bitlänge beträgt also 4.

Die Bitlänge einer natürlichen Zahl a lässt sich berechnen, indem die kleinste Zweierpotenz 2^k bestimmt wird, die größer als a ist. Für a = 13 beispielsweise ist 2⁴ = 16 diese kleinste Zweierpotenz. Der Exponent k = 4 entspricht genau der Bitlänge von a.

Aufgabe: (Berechnung der Bitlänge einer natürlichen Zahl a)

Gegeben sei folgendes Programm X:

k=0;
p=1;
while (p<=a)
{
    k=k+1;
    p=p*2;
}

Das Programm X berechnet den kleinsten Exponenten k, derart dass 2^k > a.

Ermitteln Sie die schwächste Vorbedingung Q für die Korrektheitsformel {Q} X {R} mit der Nachbedingung

R: 2^k > a

Wenn das Programm terminiert, dann ist k der kleinste Exponent, der diese Nachbedingung erfüllt, da k bei 0 beginnt und bei jedem Schleifendurchlauf um 1 größer wird.

Alternativ kann die Nachbedingung etwas komplizierter als 2^k-1 kleiner gleich a und 2^k > a gewählt werden.

Hinweis: Gehen Sie schrittweise vor. Beweisen Sie zunächst die While-Schleife, indem Sie die beiden Prämissen der Schlussregel für die While-Schleife beweisen. Ermitteln Sie aus der ersten Prämisse die Schleifeninvariante P.

Lösung:

Prämisse While1: Nachbedingung R in die Form P ¬B bringen

Es gilt

B: p kleiner gleich a

Wir müssen also die Variable p in die Nachbedingung hineinbringen. R: 2^k > a lässt sich schreiben als

R: 2^k = p und p > a

Damit hat R die Form P und ¬B und die Schleifeninvariante P lautet

P: 2^k = p

Prämisse While2: Beweis des Schleifenkörpers

{ P und B } (8)

{ 2^k = p und p kleiner gleich a } (7)

{ 2^k = p } (6)

{ 2^k+1-1 = p } (5)

k=k+1;

{ 2^k-1 = p } (4)

{ 2^k = p·2 } (3)

p=p*2;

{ 2^k = p } (2)

{ P } (1)

Von Schritt 6 nach Schritt 7 wurde eine Verschärfung vorgenommen, indem eine zusätzliche Und-Bedingung hinzugenommen wurde.

Beweis des restlichen Programms vor der Schleife

{ Q } (6)

{ true } (5)

{ 2⁰ = 1 } (4)

k=0;

{ 2^k = 1 } (3)

p=1;

{ 2^k = p } (2)

{ P } (1)

Damit ist Q: true die schwächste Vorbedingung für das Programm, oder anders ausgedrückt: Das Programm erfordert keine Vorbedingungen.

Weiter mit:

	{ `P` `B` }	(8)
	{ 2^k = `p` `p` `a` }	(7)
	{ 2^k = `p` }	(6)
	{ 2^k+1-1 = `p` }	(5)
	k=k+1;
	{ 2^k-1 = `p` }	(4)
	{ 2^k = `p`·2 }	(3)
	p=p*2;
	{ 2^k = `p` }	(2)
	{ `P` }	(1)

	{ `Q` }	(6)
	{ `true` }	(5)
	{ 2⁰ = 1 }	(4)
	k=0;
	{ 2^k = 1 }	(3)
	p=1;
	{ 2^k = `p` }	(2)
	{ `P` }	(1)