---
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*}