EiP - Blatt 03

4 files changed, 159 insertions, 0 deletions

diff --git a/ws2015/EiP/blaetter/03/H3-1.md b/ws2015/EiP/blaetter/03/H3-1.md
new file mode 100644
index 0000000..bb3d2ca
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-1.md
@@ -0,0 +1,39 @@
+---
+header-includes:
+        - \usepackage{bussproofs}
+        - \renewcommand{\implies}{\rightarrow}
+        - \EnableBpAbbreviations
+---
+# Hoare-Tripel II
+
+d)
+
+\begin{prooftree}
+\AXC{$\forall \phi \ldotp \phi \implies \phi$}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n < m)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n \leq m - 1)$}
+\RightLabel{Umformung}
+\UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n + 1 \leq m)$}
+\RightLabel{Zuweisung}
+\UIC{$ \{ 0 < n + 1 \land n < m \} $ \texttt{n = n + 1} $ \{ 0 < n \land n \leq m \} $}
+\end{prooftree}
+
+e) Nimm als Gegenbeispiel:
+
+~~~
+a = -1
+b = 0
+~~~
+
+f) Seit $\phi$ die Nachfolgerfunktion auf $\mathbb{N}$.
+
+\begin{prooftree}
+\AXC{$\forall n \in \mathbb{N} \ldotp \phi(n) > n$}
+\UIC{$1 > 0$}
+\UIC{$((x + 1) + y > x + y)$}
+\UIC{$(z = x + y) \implies ((x + 1) + y > z)$}
+\UIC{$ \{ z = x + y \} $ \texttt{ x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \land z \equiv 0 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $ \quad $ \{ z = x + y \land z \equiv 1 \mod 2 \} $ \texttt{x = x + 1} $ \{ x + y > z \} $}
+\UIC{$ \{ z = x + y \} $ \texttt{if (z \% 2 == 0) x = x + 1; else y = y + 1;} $ \{ x + y > z \} $}
+\end{prooftree}
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*}
diff --git a/ws2015/EiP/blaetter/03/H3-3.md b/ws2015/EiP/blaetter/03/H3-3.md
new file mode 100644
index 0000000..ca9fbd8
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/H3-3.md
@@ -0,0 +1,33 @@
+# Code Verständnis
+
+| Zeile | Zuweisung |
+|-------+-----------|
+|   010 | x = 42    |
+|   030 | y = 36    |
+|   070 | z = 1     |
+|   080 | z = 2     |
+|   090 | z = 3     |
+|   100 | y = 39    |
+|   120 | z = 6     |
+|   070 | z = 1     |
+|   080 | z = 2     |
+|   090 | z = 3     |
+|   100 | y = 42    |
+|   120 | z = 6     |
+|   230 | x = 53    |
+|   240 | z = 0     |
+|   250 | x = 57    |
+|   260 | y = 36    |
+|   270 | z = 1     |
+|   240 | z = 1     |
+|   250 | x = 61    |
+|   260 | y = 37    |
+|   270 | z = 2     |
+|   240 | z = 2     |
+|   250 | x = 65    |
+|   260 | y = 39    |
+|   270 | z = 3     |
+|   240 | z = 3     |
+|   250 | x = 69    |
+|   260 | y = 42    |
+|   270 | z = 4     |
diff --git a/ws2015/EiP/blaetter/03/manifest b/ws2015/EiP/blaetter/03/manifest
new file mode 100644
index 0000000..ff79ea4
--- /dev/null
+++ b/ws2015/EiP/blaetter/03/manifest
@@ -0,0 +1,3 @@
+H3-1.pdf
+H3-2.pdf
+H3-3.pdf
\ No newline at end of file