blob: bb3d2cad96048c5cf70f0b218d75c19f63326983 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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}
|
