blob: 62d8fc23b10dfbbfcdfe9f3930581b4ea074640c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
---
header-includes:
- \usepackage{bussproofs}
- \renewcommand{\implies}{\rightarrow}
- \EnableBpAbbreviations
---
# Hoare-Logik: While-Schleife II
| Schleifendurchlauf | \texttt{n} | \texttt{a} | \texttt{b} | \texttt{c} |
|--------------------+------------+------------+------------+------------|
| 0 | 5 | 0 | 0 | 1 |
| 1 | 5 | 1 | 1 | 7 |
| 2 | 5 | 8 | 2 | 19 |
| 3 | 5 | 27 | 3 | 37 |
| 4 | 5 | 64 | 4 | 61 |
| 5 | 5 | 125 | 5 | 91 |
Wir bezeichnen mit $P'$:
~~~
a = a + c
b = b + 1
c = c + 6*b
~~~
Wir bezeichnen mit $J$:
~~~
a = 0
b = 0
c = 1
~~~
und setzen $J'$ derart, dass $\{\} J \{J'\}$ gültig ist.
Wir bezeichnen zudem mit $\bar P$:
~~~
while (b != n) {
a = a + c
b = b + 1
c = c + 6*b
}
~~~
Es sei zudem $I = (c = (b + 1)^3 - b^3)$.
\begin{prooftree}
\AXC{$ 1 = (0 + 1)^3 - 0 $}
\UIC{$ (a, b, c) = (0, 0, 1) \implies c = ( b + 1 )^3 - b^3$}
\UIC{$J' \implies I$}
\end{prooftree}
\begin{prooftree}
\AXC{$0 = 0$}
\RightLabel{Algebraische Umformung}
\UIC{$(b + 1)^3 - b^3 + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$}
\UIC{$c = ( b + 1 )^3 - b^3 \implies c + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$}
\UIC{$\{c = ( b + 1 )^3 - b^3 \land b \neq n \}$ $P'$ $\{ c = (b + 1)^3 - b^3 \}$}
\UIC{$\{ I \land b \}$ $P'$ $ \{ I \} $}
\end{prooftree}
\begin{prooftree}
\AXC{$J' \implies I$}
\AXC{$\{I \land b\}$ $P'$ $\{ I \}$}
\AXC{$I \land b = n \implies a = n^3$}
\TIC{$ \{ n > 0 \land J' \} $ $ \bar P $ $ \{ a = n^3 \} $}
\end{prooftree}
Es bleibt zu zeigen, dass $a(n) = n^3$.
Es gilt wegen $P'$ und $J$:
\begin{align*}
c(0) &= 1 \\
c(k) &= c(k - 1) + 6 \cdot k \\
&= 1 + \sum_{i = 0}^{k} 6i \\
a(0) &= 0 \\
a(k) &= a(k - 1) + c(k - 1) \\
&= a(k - 1) + 1 + \sum_{i = 0}^{k - 1} 6i \\
&= \sum_{j = 0}^{k} \left ( 1 + \sum_{i = 0}^{j - 1} 6i \right ) \\
&= k + \sum_{j = 0}^{k} \sum_{i = 0}^{j - 1} 6i \\
&= k + \sum_{j = 0}^{k} \left ( 3j (j - 1) \right ) \\
&= k + \left ( k^3 - k \right ) \\
&= k^3
\end{align*}
|
