Im Folgenden werden wir die Fakultätsfunktion als imperativen Algorithmus entwerfen.
Fakultätsfunktion:
0
!
=
1
,
x
!
=
x
⋅
(
x
−
1
)
!
für
x
>
0
{\displaystyle 0!=1,x!=x\cdot (x-1)!~{\text{für}}~x>0}
F
A
C
v
a
r
X
,
Y
:
i
n
t
;
{\displaystyle FAC~var~X,Y:int;}
i
n
p
u
t
X
;
{\displaystyle inputX;}
Y
:=
1
{\displaystyle Y:=1}
w
h
i
l
e
X
>
1
d
o
Y
:=
Y
⋅
X
;
X
:=
X
−
1
{\displaystyle while~X>1~do~Y:=Y\cdot X;~X:=X-1}
o
u
t
p
u
t
Y
{\displaystyle output~Y}
Es ist:
[
[
F
A
C
]
]
(
x
)
=
{
x
!
für
x
≥
0
1
s
o
n
s
t
{\displaystyle [\![FAC]\!](x)=\left\{{\begin{array}{ll}x!&{\text{für}}~x~\geq 0\\1&sonst\end{array}}\right.}
Falls die Bedingung der while-Schleife
x
≠
0
{\displaystyle x\neq 0}
[
[
F
A
C
]
]
(
x
)
=
{
x
!
für
x
≥
0
⊥
s
o
n
s
t
{\displaystyle [\![FAC]\!](x)=\left\{{\begin{array}{ll}x!&{\text{für}}~x~\geq 0\\\bot &sonst\end{array}}\right.}
Gesucht ist das Ergebnis des Aufrufs FAC(3).
Die Abkürzung der while
β
{\displaystyle \beta }
w
h
i
l
e
X
>
1
d
o
Y
:=
Y
⋅
X
;
X
:=
X
−
1
{\displaystyle while~X>1~do~Y:=Y\cdot ~X;X:=X-1}
Die Signatur der Semantikfunktion ist
[
[
F
A
C
]
]
:
i
n
t
→
i
n
t
{\displaystyle [\![FAC]\!]:int\to int}
Die Funktion ist durch Lesen von Y im Endzustand Z definiert
[
[
F
A
C
]
]
(
w
)
=
Z
(
Y
)
{\displaystyle [\![FAC]\!](w)=Z(Y)}
Der Endzustand ist definiert durch
Z
=
[
[
α
]
]
(
Z
0
)
{\displaystyle Z=[\![\alpha ]\!](Z_{0})}
α
{\displaystyle \alpha }
Der initiale Zustand
Z
0
{\displaystyle Z_{0}}
Z
0
=
(
X
=
w
,
Y
=
⊥
)
{\displaystyle Z_{0}=(X=w,Y=\bot )}
Die Zustände abkürzend ohne Variablennamen sind
Z
0
=
(
w
,
⊥
)
{\displaystyle Z_{0}=(w,\bot )}
Z
=
[
[
α
]
]
(
Z
0
)
{\displaystyle Z=[\![\alpha ]\!](Z_{0})}
=
[
[
α
]
]
(
3
,
⊥
)
{\displaystyle =[\![\alpha ]\!](3,\bot )}
=
[
[
Y
:=
1
;
w
h
i
l
e
β
]
]
(
3
,
⊥
)
{\displaystyle =[\![Y:=1;while~\beta ]\!](3,\bot )}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
Y
:=
1
]
]
(
3
,
⊥
)
)
{\displaystyle =[\![while~\beta ]\!]([\![Y:=1]\!](3,\bot ))}
=
[
[
w
h
i
l
e
β
]
]
(
3
,
⊥
)
Y
←
1
{\displaystyle =[\![while~\beta ]\!](3,\bot )Y\leftarrow 1}
=
[
[
w
h
i
l
e
β
]
]
(
3
,
1
)
{\displaystyle =[\![while~\beta ]\!](3,1)}
=
{
Z
f
a
l
l
s
Z
(
B
)
=
f
a
l
s
e
[
[
w
h
i
l
e
B
d
o
α
′
]
]
(
[
[
α
′
]
]
(
Z
)
)
s
o
n
s
t
{\displaystyle =\left\{{\begin{array}{ll}Z&falls~Z(B)=false\\\,[\![while~B~do~\alpha ']\!]([\![\alpha ']\!](Z))&sonst\end{array}}\right.}
=
{
(
3
,
1
)
f
a
l
l
s
Z
(
X
>
1
)
=
(
3
>
1
)
=
f
a
l
s
e
[
[
w
h
i
l
e
β
]
]
(
[
[
Y
:=
Y
⋅
X
;
x
:=
X
−
1
]
]
(
Z
)
)
s
o
n
s
t
{\displaystyle =\left\{{\begin{array}{ll}(3,1)&falls~Z(X>1)=(3>1)=false\\\,[\![while~\beta ]\!]~([\![Y:=Y\cdot X;~x:=X-1]\!](Z))&sonst\end{array}}\right.}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
Y
:=
Y
⋅
X
;
X
:=
X
−
1
]
]
(
3
,
1
)
)
{\displaystyle =[\![while~\beta ]\!]([\![Y:=Y\cdot X;~X:=X-1]\!](3,1))}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
X
:=
X
−
1
]
]
(
[
[
Y
:=
Y
⋅
X
]
]
(
3
,
1
)
)
)
{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!]([\![Y:=Y\cdot X]\!](3,1)))}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
X
:=
X
−
1
]
]
(
3
,
3
)
)
{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!](3,3))}
=
[
[
w
h
i
l
e
β
]
]
(
2
,
3
)
{\displaystyle =[\![while~\beta ]\!](2,3)}
=
{
(
2
,
3
)
f
a
l
l
s
Z
(
X
>
1
)
=
(
2
>
1
)
=
f
a
l
s
e
[
[
(
w
h
i
l
e
β
)
]
]
(
[
[
Y
:=
Y
⋅
X
;
X
:=
X
−
1
]
]
(
Z
)
)
s
o
n
s
t
{\displaystyle =\left\{{\begin{array}{ll}(2,3)&falls~Z(X>1)=(2>1)=false\\\,[\![(while~\beta )]\!]~([\![Y:=Y\cdot X;~X:=X-1]\!](Z))&sonst\end{array}}\right.}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
Y
:=
Y
⋅
X
;
X
:=
X
−
1
]
]
(
2
,
3
)
)
{\displaystyle =[\![while~\beta ]\!]([\![Y:=Y\cdot X;~X:=X-1]\!](2,3))}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
X
:=
X
−
1
]
]
(
[
[
Y
:=
Y
⋅
X
]
]
(
2
,
3
)
)
)
{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!]([\![Y:=Y\cdot X]\!](2,3)))}
=
[
[
w
h
i
l
e
β
]
]
(
[
[
X
:=
X
−
1
]
]
(
2
,
6
)
)
{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!](2,6))}
=
[
[
w
h
i
l
e
β
]
]
(
1
,
6
)
{\displaystyle =[\![while~\beta ]\!](1,6)}
=
{
(
1
,
6
)
f
a
l
l
s
Z
(
X
>
1
)
=
(
1
>
1
)
=
f
a
l
s
e
[
[
(
w
h
i
l
e
β
)
]
]
(
[
[
Y
:=
Y
⋅
X
;
X
:=
X
−
1
]
]
(
Z
)
)
s
o
n
s
t
{\displaystyle =\left\{{\begin{array}{ll}(1,6)&falls~Z(X>1)=(1>1)=false\\\,[\![(while~\beta )]\!]~([\![Y:=Y\cdot X;~X:=X-1]\!](Z))&sonst\end{array}}\right.}
=
(
1
,
6
)
{\displaystyle =(1,6)}
Das bedeutet
Z
=
[
[
α
]
]
(
Z
0
)
{\displaystyle Z=[\![\alpha ]\!](Z_{0})}
=
[
[
α
]
]
(
3
,
⊥
)
{\displaystyle =[\![\alpha ]\!](3,\bot )}
...
=
(
1
,
6
)
{\displaystyle =(1,6)}
Damit gilt
[
[
F
A
C
]
]
(
3
)
=
Z
(
Y
)
=
6
{\displaystyle [\![FAC]\!](3)=Z(Y)=6}
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 Kürzel α' statt α, da α bereits verwendet wurde). Dies entspricht im Beispiel α' = {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 zur rekursiven Funktionsdefinition!
Da die Vorlesungsinhalte auf dem Buch Algorithmen und Datenstrukturen: Eine Einführung mit Java von Gunter Saake und Kai-Uwe Sattler aufbauen, empfiehlt sich dieses Buch um das hier vorgestellte Wissen zu vertiefen. Die auf dieser Seite behandelten Inhalte sind in Kapitel 3.3.3 zu finden.
![{\displaystyle [\![FAC]\!](x)=\left\{{\begin{array}{ll}x!&{\text{für}}~x~\geq 0\\1&sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3ba4024d9901d73dd55c9c70d21089cd1a7fff87)
![{\displaystyle [\![FAC]\!](x)=\left\{{\begin{array}{ll}x!&{\text{für}}~x~\geq 0\\\bot &sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/219396152e8abdf77377c24e4fd9c488ddec9b12)
![{\displaystyle [\![FAC]\!]:int\to int}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cfb789da8fe2e7be02c5850c13d0e701dc78150f)
![{\displaystyle [\![FAC]\!](w)=Z(Y)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/61d2bb477fb6afeb6285d47248f9f2200915a7d3)
![{\displaystyle Z=[\![\alpha ]\!](Z_{0})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea4ca6687b20b2d70b39578e565452b234180ab2)
![{\displaystyle =[\![\alpha ]\!](3,\bot )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4d4a5403856c43b827f023ccee91b26114bfad7f)
![{\displaystyle =[\![Y:=1;while~\beta ]\!](3,\bot )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/037335c75fff8f8d9729dc2363623a87cdaa9685)
![{\displaystyle =[\![while~\beta ]\!]([\![Y:=1]\!](3,\bot ))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3fa446c627fe591c0ab64dde39f6fd08a0c99d14)
![{\displaystyle =[\![while~\beta ]\!](3,\bot )Y\leftarrow 1}](https://wikimedia.org/api/rest_v1/media/math/render/svg/459643d9f6cc1f01550ff1b7c9ab107d3e7a0cc8)
![{\displaystyle =[\![while~\beta ]\!](3,1)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ddd7f5b84395f7118a8ec81ad6325df02821d42f)
![{\displaystyle =\left\{{\begin{array}{ll}Z&falls~Z(B)=false\\\,[\![while~B~do~\alpha ']\!]([\![\alpha ']\!](Z))&sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8b82383538b003b765c607148ad34d6a8923e40f)
![{\displaystyle =\left\{{\begin{array}{ll}(3,1)&falls~Z(X>1)=(3>1)=false\\\,[\![while~\beta ]\!]~([\![Y:=Y\cdot X;~x:=X-1]\!](Z))&sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/674dc6ac4a60cc398a09019c73629904663c418f)
![{\displaystyle =[\![while~\beta ]\!]([\![Y:=Y\cdot X;~X:=X-1]\!](3,1))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f9ccd0ad622e97dfc4ba47ae5ff195a479e8e81)
![{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!]([\![Y:=Y\cdot X]\!](3,1)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/77163f22c498e0285a042b7e188796e52ad84aba)
![{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!](3,3))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9bb98a7cd897d02102943f7ae09666308de8f3d4)
![{\displaystyle =[\![while~\beta ]\!](2,3)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5acb9206dfc90dad004476ab1d9c7cbed3929fdc)
![{\displaystyle =\left\{{\begin{array}{ll}(2,3)&falls~Z(X>1)=(2>1)=false\\\,[\![(while~\beta )]\!]~([\![Y:=Y\cdot X;~X:=X-1]\!](Z))&sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1e0cf2772ce5143a87a174ac1be999000b93b20)
![{\displaystyle =[\![while~\beta ]\!]([\![Y:=Y\cdot X;~X:=X-1]\!](2,3))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ab50e663d81fdf50e6884e6b0e638f9815348c9c)
![{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!]([\![Y:=Y\cdot X]\!](2,3)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2735e2d4660104b81312c9e22995267918601d51)
![{\displaystyle =[\![while~\beta ]\!]([\![X:=X-1]\!](2,6))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f9270f44a0e604f2a8235b9ce8a67c7c6d03d041)
![{\displaystyle =[\![while~\beta ]\!](1,6)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/80dfb61a8347c03963e5e5e8fce5478ecd501345)
![{\displaystyle =\left\{{\begin{array}{ll}(1,6)&falls~Z(X>1)=(1>1)=false\\\,[\![(while~\beta )]\!]~([\![Y:=Y\cdot X;~X:=X-1]\!](Z))&sonst\end{array}}\right.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0e1abfd85cda0503400eeb3e8a351536a12d961b)
![{\displaystyle [\![FAC]\!](3)=Z(Y)=6}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b084ee327ecf82ab1df7ce14f71f068a55df57e2)
