\documentclass{bschlangaul-aufgabe}
\bLadePakete{java,wpkalkuel}
\begin{document}
\bAufgabenMetadaten{
  Titel = {Aufgabe 1},
  Thematik = {Verifikation},
  Referenz = 66116-2020-H.T1-TA1-A1,
  RelativerPfad = Examen/66116/2020/09/Thema-1/Teilaufgabe-1/Aufgabe-1.tex,
  ZitatSchluessel = examen:66116:2020:09,
  BearbeitungsStand = mit Lösung,
  Korrektheit = unbekannt,
  Ueberprueft = {unbekannt},
  Stichwoerter = {Verifikation, wp-Kalkül},
  EinzelpruefungsNr = 66116,
  Jahr = 2020,
  Monat = 09,
  ThemaNr = 1,
  TeilaufgabeNr = 1,
  AufgabeNr = 1,
}

\let\wp=\bWpKalkuel
\let\equivalent=\bWpEquivalent
\let\erklaerung=\bWpErklaerung

\begin{enumerate}

%%
% a)
%%

\item Definieren Sie die Begriffe \emph{„partielle Korrektheit”} und
\emph{„totale Korrektheit”} und grenzen Sie sie voneinander ab.
\index{Verifikation}
\footcite{examen:66116:2020:09}

\begin{bAntwort}
\begin{description}
\item[partielle Korrektheit]

Ein Programmcode wird bezüglich einer Vorbedingung $P$ und einer
Nachbedingung $Q$ partiell korrekt genannt, wenn bei einer Eingabe, die
die Vorbedingung $P$ erfüllt, jedes Ergebnis die Nachbedingung $Q$
erfüllt. Dabei ist es noch möglich, dass das Programm nicht für jede
Eingabe ein Ergebnis liefert, also nicht für jede Eingabe terminiert.

\item[totale Korrektheit]

Ein Code wird total korrekt genannt, wenn er partiell korrekt ist und
zusätzlich für jede Eingabe, die die Vorbedingung $P$ erfüllt,
terminiert. Aus der Definition folgt sofort, dass total korrekte
Programme auch immer partiell korrekt sind.
\footcite{wiki:korrektheit}
\end{description}
\end{bAntwort}

%%
% b)
%%

\item Geben Sie die Verifikationsregel für die abweisende Schleife
\bJavaCode{while(b) { A }}
an.

\begin{bAntwort}
Eine abweisende Schleife ist eine while-Schleife, da die
Schleifenbedingung schon bei der ersten Prüfung falsch sein kann und
somit die Schleife abgewiesen wird.

Um die schwächste Vorbedingung eines Ausdrucks der Form
„\bJavaCode{while(b) { A }}“ zu finden, verwendet man eine
\emph{Schleifeninvariante}. Sie ist ein Prädikat für das

\begin{displaymath}
\{ I \wedge b \} A \{ I \}
\end{displaymath}

\noindent
gilt. Die Schleifeninvariante gilt also sowohl vor, während und nach der
Schleife.
\end{bAntwort}

%%
% c)
%%

\item Erläutern Sie kurz und prägnant die Schritte zur Verifikation
einer abweisenden Schleife mit Vorbedingung $P$ und Nachbedingung $Q$.

\begin{bAntwort}
\begin{description}
\item[Schritt 0:] Schleifeninvariante $I$ finden

\item[Schritt 1:] $I$ gilt vor Schleifenbeginn,\\
d.h: $P \Rightarrow \wp{Code vor Schleife}{I}$

\item[Schritt 2:] $I$ gilt nach jedem Schleifendurchlauf\\
d.h. $I \land b \Rightarrow \wp{Code in der Schleife}{I}$

\item[Schritt 3:]

Bei Terminierung der Schleife liefert Methode das gewünschte Ergebnis,\\
d.h. $I \,\land \neq b \Rightarrow \wp{Code nach der Schleife}{Q}$
\footcite[Seite 31]{sosy:fs:5}
\end{description}
\end{bAntwort}

%%
% d)
%%

\item Wie kann man die Terminierung einer Schleife beweisen?

\begin{bAntwort}
Zum Beweis der Terminierung einer Schleife muss eine
Terminierungsfunktion $T$ angeben werden:

\begin{displaymath}
T \colon V \rightarrow \mathbb{N}
\end{displaymath}

\noindent
$V$ ist eine Teilmenge der Ausdrücke über die Variablenwerte der
Schleife

Die Terminierungsfunktion muss folgende Eigenschaften besitzen:

\begin{itemize}
\item Ihre Werte sind natürliche Zahlen (einschließlich 0).

\item Jede Ausführung des Schleifenrumpfs verringert ihren Wert (streng
monoton fallend).

\item Die Schleifenbedingung ist false, wenn $T = 0$.
\end{itemize}

$T$ ist die obere Schranke für die noch ausstehende Anzahl von
Schleifendurchläufen.
\footcite[Seite 33]{sosy:fs:5}

Beweise für Terminierung sind nicht immer möglich!
\footcite[Seite 38]{sosy:fs:5}
\end{bAntwort}

%%
% e)
%%

\newpage

\item Geben Sie für das folgende Suchprogramm die nummerierten
Zusicherungen an. \textcolor{blue}{Lassen Sie dabei jeweils die
invariante Vorbedingung $P$ des Suchprogramms weg.}
Schreiben Sie nicht auf dem Aufgabenblatt!
\index{wp-Kalkül}

$P \equiv n > 0 \land a_0 \dots a_{n-1} \in \mathbb{Z}^n \land m \in \mathbb{Z}$

% i = -1;
% // (1)
% j = 0;
% // (2)
% while (i == -1 && j < n) // (3)
% { // (4)
%   if (a[j] == m) {
%     // (5)
%     i = j;
%     // (6)
%   }
%   else {
%     // (7)
%     j = j + 1;
%     // (8)
%   }
%   // (9)
% }
% \end{minted}

\bJavaExamen[firstline=18,lastline=34]{66116}{2020}{09}{Verfikation}

$Q \equiv P \land (i = -1 \land \forall \, 0 \leq k < n \colon a_k \neq m) \lor
 (i \geq 0 \land a_i = m)$

\begin{bAntwort}
In dieser Aufgabenstellung fällt die Vorbedingung mit der Invariante
zusammen. Es muss kein wp-Kalkül berechnet werden, sondern „nur“ die
Zuweisungen nachverfolgt werden, um zum Schluss die Nachbedingung zu
erhalten.

% markierung
\def\m#1{\textcolor{blue}{#1}}
\def\tmp{ $\textcolor{blue}{\land \, P}$}

{
\renewcommand{\labelenumii}{\arabic{enumii}.}
\begin{enumerate}
\item $(i = -1)$ \tmp % 1
\item
  $(i = -1) \land
  (j = 0)$
  \tmp % 2
\item
  $(i = -1) \land
  (0 \leq j < n)$
  \tmp % 3
\item
  $(i = -1) \land
  (0 \leq j < n)$
  \tmp % 4
\item
  $(i = -1) \land
  (a_j = m) \land
  (0 \leq j < n)$
  \tmp % 5
\item
  $(i \geq 0) \land
  i = j \land
  (a_j = m) \land
  (0 \leq j < n)$
  \tmp  % 6
\item
  $(i = -1) \land
  (\forall \, 0 \leq j < n \colon a_j \neq m)$
  \tmp % 7
\item
  $(i = -1) \land
  (\forall \, 0 < j \leq n \colon a_j \neq m)$
  \tmp % 8
\item
  $((i = -1) \land
  (\forall \, 0 \leq k < j \colon a_k \neq m)) \lor
  ((i \geq 0) \land (a_i = m))$ \tmp % 9
\end{enumerate}
}
\end{bAntwort}

\begin{bAdditum}[Code-Beispiel eingebaut in eine Java-Klasse]
\bJavaExamen{66116}{2020}{09}{Verfikation}
\end{bAdditum}

\end{enumerate}
\end{document}