\documentclass{bschlangaul-aufgabe}
\bLadePakete{mathe,tabelle,syntax}
\begin{document}
\bAufgabenMetadaten{
  Titel = {Aufgabe zum Grundwissen},
  Thematik = {Grundwissen},
  Referenz = SOSY.Testen.Formale-Verifikation.Grundwissen,
  RelativerPfad = Module/40_SOSY/05_Testen/10_Formale-Verifikation/Aufgabe_Grundwissen.tex,
  ZitatSchluessel = sosy:ab:8,
  ZitatBeschreibung = {Seite 1},
  BearbeitungsStand = mit Lösung,
  Korrektheit = unbekannt,
  Ueberprueft = {unbekannt},
  Stichwoerter = {Formale Verifikation, wp-Kalkül, Hoare-Kalkül, Partielle Korrektheit, Totale Korrektheit, Invariante, Terminierungsfunktion},
}

\begin{enumerate}

%%
% (a)
%%

\item Geben Sie zwei verschiedene Möglichkeiten der formalen
Verifikation\index{Formale Verifikation} an.
\footcite[Seite 1]{sosy:ab:8}

\begin{bAntwort}
\begin{description}
\item[1. Möglichkeit:]

formale Verifikation mittels \emph{vollständiger Induktion} (eignet sich
bei \emph{rekursiven} Programmen).

\item[2. Möglichkeit:]

formale Verifikation mittels \emph{wp-Kalkül}\index{wp-Kalkül} oder
\emph{Hoare-Kalkül}\index{Hoare-Kalkül} (eignet sich bei
\emph{iterativen} Programmen).
\end{description}
\end{bAntwort}

%%
% (b)
%%

\item Erläutern Sie den Unterschied von partieller\index{Partielle
Korrektheit} und totaler Korrektheit\index{Totale Korrektheit}.

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

Das Programm verhält sich spezifikationsgemäß, \emph{falls} es
terminiert.

\item[totale Korrektheit:]

Das Programm verhält sich spezifikationsgemäß und es \emph{terminiert
immer}.
\end{description}
\end{bAntwort}

%%
% (c)
%%

\item Gegeben sei die Anweisungssequenz $A$. Sei $P$ die Vorbedingung
und $Q$ die Nachbedingung dieser Sequenz. Erläutern Sie, wie man die
(partielle) Korrektheit dieses Programmes nachweisen kann.

\begin{bAntwort}
\begin{tabular}{|>{\raggedright\arraybackslash}p{6cm}|l|l|}
Vorgehen & Horare-Kalkül & \text{wp}-Kalkül \\\hline

Wenn die Vorbedingung $P$ zutrifft, gilt nach der Ausführung der
Anweisungssequenz $A$ die Nachbedingung $Q$. &

$\{P\}A\{Q\}$ &

$P \Rightarrow \text{\text{wp}}(A,Q)$

\end{tabular}
\end{bAntwort}

%%
% (d)
%%

\item Gegeben sei nun folgendes Programm:

\begin{minted}{python}
A_1
while(b):
    A_2
A_3
\end{minted}

wobei $A_1$, $A_2$, $A_3$ Anweisungssequenzen sind. Sei $P$ die
Vorbedingung und $Q$ die Nachbedingung des Programms. Die
Schleifeninvariante\index{Invariante} der while-Schleife wird mit $I$
bezeichnet. Erläutern Sie, wie man die (partielle) Korrektheit dieses
Programmes nachweisen kann.

\begin{bAntwort}
\begin{tabular}{|>{\raggedright\arraybackslash}p{3.8cm}|l|l|}
Vorgehen & Horare-Kalkül & \text{wp}-Kalkül \\\hline

Die Invariante $I$ gilt vor Schleifeneintritt. &
$\{P\} A_1 \{I\}$ &
$P \Rightarrow \text{\text{wp}}(A_1,I)$\\\hline

$I$ ist invariant, d. h. $I$ gilt nach jedem Schleifendurchlauf.&
$\{I \land b\} A_2 \{I\}$ &
$I \land b \Rightarrow \text{\text{wp}}(A_2, I)$\\\hline

Die Nachbedingung $Q$ wird erfüllt.&
$\{I \land \neg b\} A_3 \{Q\}$ &
$I \land \neg b \Rightarrow \text{\text{wp}}(A_3, I)$\\
\end{tabular}
\end{bAntwort}

%%
% (e)
%%

\item Beschreiben Sie, welche Vorraussetzungen eine
Terminierungsfunktion\index{Terminierungsfunktion} erfüllen muss, damit
die totale Korrektheit gezeigt werden kann.

\begin{bAntwort}
Mit einer Terminierungsfunktion $T$ kann bewiesen werden, dass eine
Wiederholung terminiert. Sie ist eine Funktion, die

\begin{itemize}
\item ganzzahlig,

\item nach unten beschränkt (die Schleifenbedingung ist \emph{false},
wenn $T = 0$) und

\item streng monoton fallend (jede Ausführung der Wiederholung
verringert ihren Wert)

ist.

\end{itemize}
Im Hoare-Kalkül muss $\{I \land b \land (T = n)\} A \{T < n\}$ gezeigt
werden, im wp-Kalkül $I \Rightarrow T \geq
0$.
\bFussnoteUrl{https://osg.informatik.tu-chemnitz.de/lehre/aup/
aup-07-AlgorithmenEntwurf-script_de.pdf}
\end{bAntwort}

\end{enumerate}
\end{document}