\begin{slide}{Axiomatische Semantik}

Notation für Aussagen über Programmzustände:
\begin{verbatim}
{ V } A { N }
\end{verbatim}

\begin{itemize}\itemsep 2pt
\item für jeden Zustand $s$, 
  in dem Vorbedingung $V$ gilt:
\item wenn  Anweisung A ausgeführt wird,
\item  und Zustand $t$ erreicht wird,
 dann gilt dort Nachbedingung $N$
\end{itemize}

Beispiel:
\begin{verbatim}
{ x >= 5 } y := x + 3 { y >= 7 }
\end{verbatim}

Gültigkeit solcher Aussagen kann man
\begin{itemize}
\item beweisen (mit Hoare-Kalkül)
\item prüfen (testen)
\end{itemize}

\end{slide}

\begin{slide}{Eiffel}

Bertrand Meyer, \url{http://www.eiffel.com/}

\begin{verbatim}
class Stack [G]     feature 
    count : INTEGER
    item : G is require not empty do ... end
    empty : BOOLEAN is do .. end
    full  : BOOLEAN is do .. end
    put (x: G) is
       require not full do ...
       ensure not empty
              item = x
              count = old count + 1
\end{verbatim}
Beispiel sinngemäß aus: B. Meyer: 
Object Oriented Software Construction,
Prentice Hall 1997

\end{slide}


\begin{slide}{Hoare-Kalkül}


Kalkül: für jede Anweisung ein Axiom,
das die schwächste Vorbedingung
(weakest precondition) beschreibt.

\renewcommand{\wp}{\operatorname{wp}}

Beispiele
\begin{itemize}
\item
  \verb| { N[x/E] } x := E { N } |
\item
\begin{verbatim}
    { V und     B } C { N }  
und { V und not B } D { N }
=>  { V } if (B) then C else D { N }
\end{verbatim}
\item
  Schleife \dots benötigt Invariante
\end{itemize}

\end{slide}



%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
