From ab9484b343abd995cba915bb0ba4be8907dfa6ec Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Fri, 13 Nov 2015 23:45:26 +0000 Subject: Shorter lecture names --- 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 deletions(-) delete mode 100644 ws2015/EiP/blaetter/03/H3-1.md delete mode 100644 ws2015/EiP/blaetter/03/H3-2.md delete mode 100644 ws2015/EiP/blaetter/03/H3-3.md delete mode 100644 ws2015/EiP/blaetter/03/manifest (limited to 'ws2015/EiP/blaetter/03') diff --git a/ws2015/EiP/blaetter/03/H3-1.md b/ws2015/EiP/blaetter/03/H3-1.md deleted file mode 100644 index bb3d2ca..0000000 --- a/ws2015/EiP/blaetter/03/H3-1.md +++ /dev/null @@ -1,39 +0,0 @@ ---- -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 deleted file mode 100644 index 62d8fc2..0000000 --- a/ws2015/EiP/blaetter/03/H3-2.md +++ /dev/null @@ -1,84 +0,0 @@ ---- -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 deleted file mode 100644 index ca9fbd8..0000000 --- a/ws2015/EiP/blaetter/03/H3-3.md +++ /dev/null @@ -1,33 +0,0 @@ -# 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 deleted file mode 100644 index ff79ea4..0000000 --- a/ws2015/EiP/blaetter/03/manifest +++ /dev/null @@ -1,3 +0,0 @@ -H3-1.pdf -H3-2.pdf -H3-3.pdf \ No newline at end of file -- cgit v1.2.3