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-1.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-1.md')
-rw-r--r-- | ws2015/EiP/blaetter/03/H3-1.md | 39 |
1 files changed, 0 insertions, 39 deletions
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 @@ | |||
1 | --- | ||
2 | header-includes: | ||
3 | - \usepackage{bussproofs} | ||
4 | - \renewcommand{\implies}{\rightarrow} | ||
5 | - \EnableBpAbbreviations | ||
6 | --- | ||
7 | # Hoare-Tripel II | ||
8 | |||
9 | d) | ||
10 | |||
11 | \begin{prooftree} | ||
12 | \AXC{$\forall \phi \ldotp \phi \implies \phi$} | ||
13 | \UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n < m)$} | ||
14 | \RightLabel{Umformung} | ||
15 | \UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n \leq m - 1)$} | ||
16 | \RightLabel{Umformung} | ||
17 | \UIC{$(0 < n + 1 \land n < m) \implies (0 < n + 1 \land n + 1 \leq m)$} | ||
18 | \RightLabel{Zuweisung} | ||
19 | \UIC{$ \{ 0 < n + 1 \land n < m \} $ \texttt{n = n + 1} $ \{ 0 < n \land n \leq m \} $} | ||
20 | \end{prooftree} | ||
21 | |||
22 | e) Nimm als Gegenbeispiel: | ||
23 | |||
24 | ~~~ | ||
25 | a = -1 | ||
26 | b = 0 | ||
27 | ~~~ | ||
28 | |||
29 | f) Seit $\phi$ die Nachfolgerfunktion auf $\mathbb{N}$. | ||
30 | |||
31 | \begin{prooftree} | ||
32 | \AXC{$\forall n \in \mathbb{N} \ldotp \phi(n) > n$} | ||
33 | \UIC{$1 > 0$} | ||
34 | \UIC{$((x + 1) + y > x + y)$} | ||
35 | \UIC{$(z = x + y) \implies ((x + 1) + y > z)$} | ||
36 | \UIC{$ \{ z = x + y \} $ \texttt{ x = x + 1} $ \{ x + y > z \} $} | ||
37 | \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 \} $} | ||
38 | \UIC{$ \{ z = x + y \} $ \texttt{if (z \% 2 == 0) x = x + 1; else y = y + 1;} $ \{ x + y > z \} $} | ||
39 | \end{prooftree} | ||