From 46bff23a54eef783610ecb98070de2368a8c9192 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Sat, 7 Nov 2015 14:00:29 +0000 Subject: EiP - Blatt 03 --- ws2015/EiP/blaetter/03/H3-1.md | 39 +++++++++++++++++++ ws2015/EiP/blaetter/03/H3-2.md | 84 +++++++++++++++++++++++++++++++++++++++++ ws2015/EiP/blaetter/03/H3-3.md | 33 ++++++++++++++++ ws2015/EiP/blaetter/03/manifest | 3 ++ 4 files changed, 159 insertions(+) create mode 100644 ws2015/EiP/blaetter/03/H3-1.md create mode 100644 ws2015/EiP/blaetter/03/H3-2.md create mode 100644 ws2015/EiP/blaetter/03/H3-3.md create mode 100644 ws2015/EiP/blaetter/03/manifest (limited to 'ws2015') 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 -- cgit v1.2.3