Formale Verifikation - Aufgaben

Ein Polynom ist ein Ausdruck der Form a_n·xⁿ + a_n-1·x^n-1 +  ...  + a₀·x⁰, also zum Beispiel

p  =  2·x³ + 5·x + 4.

Die Zahlen a_i heißen Koeffizienten des Polynoms. Das Polynom p aus dem Beispiel hat die Koeffizienten a₃ = 2, a₂ = 0, a₁ = 5, a₀ = 4.

Ist xⁿ die höchste Potenz des Polynoms mit Koeffizient a_n ≠ 0, so ist n der Grad des Polynoms. Das Polynom p aus dem Beispiel hat den Grad 3.

Ein Polynom lässt sich als Funktion f(x) auf­fassen. Wenn für die Variable x eine Zahl eingesetzt wird, lässt sich das Polynom auswerten, das heißt es lässt sich der Funktions­wert berechnen. Indem zum Beispiel in das Polynom p für x die Zahl 2 eingesetzt wird, ergibt sich der Funktions­wert 2·2³ + 5·2 + 4 = 16 + 10 + 4 = 30.

Polynomauswertung nach dem Horner-Schema

Ein Polynom lässt sich auch auf eine etwas andere Weise auswerten, als es seine Darstellung als gewichtete Summe von Potenzen nahelegt, nämlich nach dem Horner-Schema.

Nach dem Horner-Schema wird das Polynom p aus dem Beispiel für x = 2 wie folgt ausgewertet (die Koeffizienten sind rot dargestellt):

(((0 · 2 + 2) · 2 + 0) · 2 + 5) · 2 + 4  =  (8 + 5) · 2 + 4  =  26 + 4  =  30

Programm

Das folgende Programm X wertet ein Polynom vom Grad n mit den Koeffizienten a[n], ..., a[0] an der Stelle x nach dem Horner-Schema aus. Das Ergebnis der Auswertung ist der Wert von s nach Ende der Berechnung.

Mit dem Polynom p aus dem Beispiel, also mit n = 3, den Koeffizienten 2, 0, 5, 4 und der Zahl x = 2 berechnet das Programm somit den Funktions­wert s = 30.

Beweis der Korrektheit des Programms

Mit X bezeichnen wir das ganze Programm, mit W die While-Schleife, mit B die Schleifen­bedingung und mit S den Schleifen­körper.

Zu beweisen ist die partielle Korrektheit von X bezüglich einer Vorbedingung Q und der Nach­bedingung

R:   s  =   _{j = 0, ..., n}  a_j · x^j

Zunächst beweisen wir die While-Schleife W; hierbei zugrunde gelegt wird die Schlussregel für die While-Schleife.

Zuerst bringen wir die Nach­bedingung R in die Form P ∧ ¬B:

P ∧ ¬B:   s  =   _{j = 0, ..., n-i}  a_i+j · x^j  ∧  i ≥ 0  ∧  i ≤ 0

Dann beweisen wir den Schleifen­körper S mit der Schleifen­invariante

P:   s  =   _{j = 0, ..., n-i}  a_i+j · x^j  ∧  i ≥ 0

Wie immer wird der Beweis von unten nach oben geführt, also beginnend bei Zeile (1).

	{ P ∧ B }	(14)
	{ s  =   j = 0, ..., n-i  ai+j · xj  ∧  i ≥ 0  ∧  i > 0 }	(13)
	{ s  =   j = 0, ..., n-i  ai+j · xj  ∧  i > 0 }	(12)
	{ s  =   j = 0, ..., n-i  ai+j · xj  ∧  i ≥ 1 }	(11)
	{ s  =   j = 0, ..., n-i+1-1  ai-1+j+1 · xj  ∧  i-1 ≥ 0 }	(10)
	i=i-1;
	{ s  =   j = 0, ..., n-i-1  ai+j+1 · xj  ∧  i ≥ 0 }	(9)
	{ s  =   j = 0, ..., n-i-1  ai+j+1 · xj + ai · x-1 – ai · x-1  ∧  i ≥ 0 }	(8)
	{ s  =   j = -1, ..., n-i-1  ai+j+1 · xj – ai · x-1  ∧  i ≥ 0 }	(7)
	{ s·x  =   j = -1, ..., n-i-1  ai+j+1 · xj+1 – ai  ∧  i ≥ 0 }	(6)
	{ s·x + ai  =   j = -1, ..., n-i-1  ai+j+1 · xj+1  ∧  i ≥ 0 }	(5)
	s=s*x + a[i];
	{ s  =   j = -1, ..., n-i-1  ai+j+1 · xj+1  ∧  i ≥ 0 }	(4)
	{ s  =   j+1 = 0, ..., n-i  ai+j+1 · xj+1  ∧  i ≥ 0 }	(3)
	{ s  =   j = 0, ..., n-i  ai+j · xj  ∧  i ≥ 0 }	(2)
	{ P }	(1)

Von Zeile (2) zu Zeile (3) wird für j eine Indexverschiebung um 1 durchgeführt, indem j durch j+1 ersetzt wird.

In Zeile (8) ist der Summand für j = -1 aus der Summe ausgekoppelt. Zeile (13) ist eine (hier nur formale) Verschärfung von Zeile (12) durch Hinzunahme einer Und-Bedingung.

Es folgt der Beweis des restlichen Teils des Programms oberhalb der While-Schleife, wiederum von unten nach oben geführt.

	{ Q }	(8)
	{ n ≥ 0 }	(7)
	{ n+1 ≥ 0 }	(6)
	{ true  ∧  n+1 ≥ 0 }	(5)
	{ 0  =   j = 0, ..., n-n-1  an+1+j · xj  ∧  n+1 ≥ 0 }	(4)
	i=n+1;
	{ 0  =   j = 0, ..., n-i  ai+j · xj  ∧  i ≥ 0 }	(3)
	s=0;
	{ s  =   j = 0, ..., n-i  ai+j · xj  ∧  i ≥ 0 }	(2)
	{ P }	(1)

Als Vorbedingung Q des Programms X ergibt sich also Q:  n ≥ 0, wobei n der Grad des Polynoms ist. Tatsächlich kommt das Programm auch mit n < 0 zurecht, wobei dann das Nullpolynom ausgewertet wird.

Totale Korrektheit

Wir haben soeben die sogenannte partielle Korrektheit des Programms bewiesen, nämlich dass es korrekt ist, sofern es terminiert. Nun beweisen wir noch, dass das Programm auch tatsächlich terminiert. Damit erbringen wir den Beweis der sogenannten totalen Korrektheit.

Für den Beweis der totalen Korrektheit benötigen wir einen ganzzahligen Ausdruck E, der im Schleifen­körper vermindert wird und für den gilt

P ∧ B ⇒ E > 0.

Offen­sichtlich ist E: i ein solcher Ausdruck.

Ferner ist zu zeigen:

{P ∧ B} z=E; S {E < z}.

Mit  E: i  lässt sich der Beweis wie folgt führen, wiederum von unten nach oben:

	{ P ∧ B }	(7)
	{ true }	(6)
	{ i-1 < i }	(5)
	z=i;
	{ i-1 < z }	(4)
	i=i-1;
	{ i < z }	(3)
	s=s*x + a[i];
	{ i < z }	(2)
	{ E < z }	(1)