diff options
author | Gregor Kleen <gkleen@yggdrasil.li> | 2015-11-13 23:45:26 +0000 |
---|---|---|
committer | Gregor Kleen <gkleen@yggdrasil.li> | 2015-11-13 23:45:26 +0000 |
commit | ab9484b343abd995cba915bb0ba4be8907dfa6ec (patch) | |
tree | f441968094bec070499d24e45e8a29f1315da1f4 /ws2015/EiP/blaetter/03/H3-2.md | |
parent | 14dc76bda755c850f859a4b974c793e694f2b0b4 (diff) | |
download | uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.gz uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.bz2 uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.tar.xz uni-ab9484b343abd995cba915bb0ba4be8907dfa6ec.zip |
Shorter lecture names
Diffstat (limited to 'ws2015/EiP/blaetter/03/H3-2.md')
-rw-r--r-- | ws2015/EiP/blaetter/03/H3-2.md | 84 |
1 files changed, 0 insertions, 84 deletions
diff --git a/ws2015/EiP/blaetter/03/H3-2.md b/ws2015/EiP/blaetter/03/H3-2.md deleted file mode 100644 index 62d8fc2..0000000 --- a/ws2015/EiP/blaetter/03/H3-2.md +++ /dev/null | |||
@@ -1,84 +0,0 @@ | |||
1 | --- | ||
2 | header-includes: | ||
3 | - \usepackage{bussproofs} | ||
4 | - \renewcommand{\implies}{\rightarrow} | ||
5 | - \EnableBpAbbreviations | ||
6 | --- | ||
7 | # Hoare-Logik: While-Schleife II | ||
8 | |||
9 | | Schleifendurchlauf | \texttt{n} | \texttt{a} | \texttt{b} | \texttt{c} | | ||
10 | |--------------------+------------+------------+------------+------------| | ||
11 | | 0 | 5 | 0 | 0 | 1 | | ||
12 | | 1 | 5 | 1 | 1 | 7 | | ||
13 | | 2 | 5 | 8 | 2 | 19 | | ||
14 | | 3 | 5 | 27 | 3 | 37 | | ||
15 | | 4 | 5 | 64 | 4 | 61 | | ||
16 | | 5 | 5 | 125 | 5 | 91 | | ||
17 | |||
18 | Wir bezeichnen mit $P'$: | ||
19 | |||
20 | ~~~ | ||
21 | a = a + c | ||
22 | b = b + 1 | ||
23 | c = c + 6*b | ||
24 | ~~~ | ||
25 | |||
26 | Wir bezeichnen mit $J$: | ||
27 | |||
28 | ~~~ | ||
29 | a = 0 | ||
30 | b = 0 | ||
31 | c = 1 | ||
32 | ~~~ | ||
33 | |||
34 | und setzen $J'$ derart, dass $\{\} J \{J'\}$ gültig ist. | ||
35 | |||
36 | Wir bezeichnen zudem mit $\bar P$: | ||
37 | |||
38 | ~~~ | ||
39 | while (b != n) { | ||
40 | a = a + c | ||
41 | b = b + 1 | ||
42 | c = c + 6*b | ||
43 | } | ||
44 | ~~~ | ||
45 | |||
46 | Es sei zudem $I = (c = (b + 1)^3 - b^3)$. | ||
47 | |||
48 | \begin{prooftree} | ||
49 | \AXC{$ 1 = (0 + 1)^3 - 0 $} | ||
50 | \UIC{$ (a, b, c) = (0, 0, 1) \implies c = ( b + 1 )^3 - b^3$} | ||
51 | \UIC{$J' \implies I$} | ||
52 | \end{prooftree} | ||
53 | |||
54 | \begin{prooftree} | ||
55 | \AXC{$0 = 0$} | ||
56 | \RightLabel{Algebraische Umformung} | ||
57 | \UIC{$(b + 1)^3 - b^3 + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$} | ||
58 | \UIC{$c = ( b + 1 )^3 - b^3 \implies c + 6 \cdot (b + 1) = (b + 2)^3 - (b + 1)^3$} | ||
59 | \UIC{$\{c = ( b + 1 )^3 - b^3 \land b \neq n \}$ $P'$ $\{ c = (b + 1)^3 - b^3 \}$} | ||
60 | \UIC{$\{ I \land b \}$ $P'$ $ \{ I \} $} | ||
61 | \end{prooftree} | ||
62 | |||
63 | \begin{prooftree} | ||
64 | \AXC{$J' \implies I$} | ||
65 | \AXC{$\{I \land b\}$ $P'$ $\{ I \}$} | ||
66 | \AXC{$I \land b = n \implies a = n^3$} | ||
67 | \TIC{$ \{ n > 0 \land J' \} $ $ \bar P $ $ \{ a = n^3 \} $} | ||
68 | \end{prooftree} | ||
69 | |||
70 | Es bleibt zu zeigen, dass $a(n) = n^3$. | ||
71 | Es gilt wegen $P'$ und $J$: | ||
72 | \begin{align*} | ||
73 | c(0) &= 1 \\ | ||
74 | c(k) &= c(k - 1) + 6 \cdot k \\ | ||
75 | &= 1 + \sum_{i = 0}^{k} 6i \\ | ||
76 | a(0) &= 0 \\ | ||
77 | a(k) &= a(k - 1) + c(k - 1) \\ | ||
78 | &= a(k - 1) + 1 + \sum_{i = 0}^{k - 1} 6i \\ | ||
79 | &= \sum_{j = 0}^{k} \left ( 1 + \sum_{i = 0}^{j - 1} 6i \right ) \\ | ||
80 | &= k + \sum_{j = 0}^{k} \sum_{i = 0}^{j - 1} 6i \\ | ||
81 | &= k + \sum_{j = 0}^{k} \left ( 3j (j - 1) \right ) \\ | ||
82 | &= k + \left ( k^3 - k \right ) \\ | ||
83 | &= k^3 | ||
84 | \end{align*} | ||