EiP - Blatt 03

1 files changed, 84 insertions, 0 deletions

diff --git a/ws2015/EiP/blaetter/03/H3-2.md b/ws2015/EiP/blaetter/03/H3-2.md
new file mode 100644
index 0000000..62d8fc2
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-2.md
@@ -0,0 +1,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*}