Читать книгу Algorithmen und Datenstrukturen - Gunter Saake - Страница 96

Die Fakultätfunktion, definiert durch 0! = 1 und x! = x · (x − 1)! für x > 0, kann wie folgt realisiert werden:

FAC:	var X,Y: int;
	input X;
	Y:=1;whileX>1doY:=Y · X;X:=X-1 od
	outputY

In dieser Realisierung gilt:

Setzt man als Bedingung für die while-Schleife »X ≠ 0«, so erhält man als Semantik des modifizierten Algorithmus FAC 2 die folgende Funktion:

Wie auch bei applikativen Algorithmen sind die booleschen Tests wichtig zur Kontrolle des Definitionsbereichs.

Für Leser mit Programmiererfahrung ist der imperative Algorithmus sicherlich sofort verständlich und auch die Vorgehensweise des Algorithmus sofort klar. Er setzt die Problemstellung in ein Berechnungsverfahren um, indem eine Variable beginnend mit dem Eingabewert in einer Schleife jeweils um 1 erniedrigt wird und die dadurch erhaltenen Folge n, (n − 1), (n − 2) … 3, 2, 1 in einer zweiten Variablen aufmultipliziert wird.

Zustandstransformation

Die formale Semantik in Form der Zustandstransformation ist sicherlich nicht sofort einsichtig. Wir werden daher die Semantik imperativer Algorithmen anhand dieses einfachen Beispiels erläutern.

Die folgenden Ausführungen verdeutlichen anhand des imperativen Algorithmus FAC aus Beispiel 3.19 die Festlegungen der Definition der formalen Semantik. Gesucht ist hierbei das Ergebnis des Aufrufs FAC (3).

Wir verwenden die Abkürzung while β für die Zeile

while X>1 do Y:=Y · X; X:=X-1 od

Signatur

Die Signatur der Semantikfunktion ist wie folgt, da es je eine Eingabe- und Ausgabevariable gibt:

FAC : int → int

Die Funktion selbst ist durch Lesen des Wertes von Y im Endzustand Z definiert:

FAC(w) = Z(Y)

Der Endzustand Z ist dabei laut Definition definiert durch folgende Gleichung:

Z = α(Z₀)

wobei α die Folge aller Anweisungen des Algorithmus ist. Der initiale Zustand Z₀ ist definiert als Z₀ = (X = w, Y = ⊥). Zustände werden wir im Folgenden abkürzend ohne Variablennamen notieren, also Z₀ = (w, ⊥).

Auswertung von FAC(3)

Gesucht sei nun FAC(3). Dazu müssen wir den Endzustand Z bestimmen. Die Bestimmung von Z, die den Definitionen der einzelnen Bausteine imperativer Algorithmen folgt, ist in Abbildung 3–1 ausführlich dargestellt. Die doch etwas umfangreiche Ableitung der Erläuterungen zur Auswertung von FAC(3) in Abbildung 3–1 bedarf einiger Bemerkungen:

 Der Übergang von der 3. auf die 4. Zeile folgt der Definition der Sequenz, indem der Sequenzoperator in einen geschachtelten Funktionsaufruf umgesetzt wird.

 Nur in der 5. Zeile wurde eine Wertzuweisung formal umgesetzt, später sind sie einfach verkürzt direkt ausgerechnet.

 In der 7. Zeile haben wir die Originaldefinition der Iteration eingesetzt (nur mit dem Kürzel α′ statt α, da α bereits verwendet wurde). Im Beispiel giltα′ = {Y := Y · X; X : X − 1}

 Das Z in der 7. und 8. Zeile steht für den Zustand (3,1) (in späteren Zeilen analog für den jeweils aktuellen Zustand).

 Bei diesem Beispiel sieht man Folgendes sehr deutlich: Die Ausführung einer While-Schleife erfolgt analog einer rekursiven Funktionsdefinition!

Damit gilt:

FAC(3) = Y(Z) = Y(X = 1, Y = 6) = 6

Z	=	α(Z0)
	=	α(3, ⊥)
	=	Y := 1; while β(3, ⊥)
	=	while β(Y := 1(3, ⊥))
	=	while β((3, ⊥)Y ← 1)
	=	while β(3, 1)
	=
	=
	=	while β(Y := Y · X; X := X − 1(3, 1))
	=	while β(X := X − 1(Y := Y · X(3, 1)))
	=	while β(X := X − 1(3, 3))
	=	while β(2, 3)
	=
	=	while β(Y := Y · X; X := X − 1(2, 3))
	=	while β(X := X − 1(Y := Y · X(2, 3)))
	=	while β(X := X − 1(2, 6))
	=	while β(1, 6)
	=
	=	(1, 6)

Abb. 3–1 Semantik imperativer Algorithmen am Beispiel

Die Umsetzung in einen imperativen Algorithmus entspricht in der Regel nicht der direkten applikativen Realisierung, da Zwischenergebnisse in Variablen vorgehalten werden können. Dieses Prinzip lässt sich sehr gut an folgendem Beispiel darstellen.