\begin{slide}{Verifikation}

Betrachte Aussagen der Form \verb|{V} P {N}| für
\begin{itemize}
\item Aussagen V, N (Vor- und Nachbedingung)
\item Programm P
\end{itemize}
\glqq wenn V gilt, und P ausgeführt wird, gilt danach N \grqq

Beispiel: \verb|{x < 0 und y > 0} x = y - x; {x > 0}|

Frage: was ist die \emph{schwächste Vorbedingung} $V$, 
so daß \verb|{ V } x = y - x; {x > 0}|?

Antwort (geraten): \verb|y > x|. 

Aus \emph{tatsächlicher Vorbedingun} \verb|x < 0 und y > 0|
folgt \verb|y>x|, also ist o. g. Beispiel-Aussage wahr.

Statt \emph{raten}: \emph{rechnen} mit Regeln.
\end{slide}

\begin{slide}{Schlußregel: Implikation}

Vorbedingung verschärfen, Nachbedingung abschwächen
\begin{verbatim}
V' => V,  N => N',  {V} P {N}
-----------------------------
       {V'} P {N'}
\end{verbatim}

\end{slide}

\begin{slide}{Axiom: Zuweisung}
\begin{verbatim}
{ N [x := A] } x = A { N }
\end{verbatim}

Beispiel: 
zeige \verb|{x < 0 und y > 0} x = y - x; {x > 0}|

\begin{verbatim}
N = (x > 0), A = (y - x)

N [x := A ] = (x > 0) [x := (y-x) ]
            = (y-x) > 0 = (y > x)

{ y > x } x = y - x { x > 0 }
\end{verbatim}

\verb|{x < 0 und y > 0}|
ist eine Verschärfung der Vorbedingung 
\verb|{y > x}|

\end{slide}

\begin{slide}{Regel: Sequenz}

\begin{verbatim}
{V} P {M}, {M} Q {N}
--------------------
   {V} P ; Q {N}
\end{verbatim}


Aufgabe: beweise
\begin{verbatim}
{ x = A und y = B }
x = x + y; y = x - y; x = x - y;
{ x = B und y = A }
\end{verbatim}

\end{slide}



\begin{slide}{Regel: Verzweigung}

\begin{verbatim}
{ V und       B } P { N }, 
{ V und nicht B } Q { N } 
--------------------------
{V} if B then P else Q {N}
\end{verbatim}

Beispiel:
\begin{verbatim}
{ } 
if x < y then z = x else z = y 
{ z = min(x,y) }
\end{verbatim}

% Aufgabe: in \verb|median5| 
% die geeigneten Bedingungen einfügen

\end{slide}

\begin{slide}{Regel: Schleifen}

\begin{verbatim}
       { V und B } P { V }
------------------------------------
{ V } while B do P { V und nicht B }
\end{verbatim}
  
\verb|V| heißt \emph{Invariante} der Schleife

Beispiel: beweise \verb|power (b,e) = b^e| 
\begin{verbatim}
static int power (int b, int e) {
  int p = 1; // B = b, E = e
  while (e > 0) { // inv: B^E = b^e * p
    if (odd (e)) { p = p * b; }
    b = b * b; e = e / 2; // abgerundet
  }
  return p;
}
\end{verbatim}


\end{slide}

\begin{slide}{Invarianten finden?}

Für gegebene Schleifen sind Invarianten schwer zu finden.

Deswegen (\glqq Extreme Programming\grqq\ a la Hoare, Dijkstra):
\begin{itemize}
\item
  \emph{erst} die Invariante hinschreiben
\item
  \emph{dann} den Schleifenkörper passend programmieren
\end{itemize}

Oft sind Invarianten durch Datenstrukturen vorgegeben
(Baum soll heap-geordnet oder balanciert oder Suchbaum sein)

Beispiel Heap-sort. Struktur-Invariante ist:

\( \forall 1 < k < n: a[ \lfloor k/2 \rfloor ] \ge a[k] \)

\end{slide}

