\begin{slide}{Axiomatische Semantik}

Hoare-Kalkül 

\begin{verbatim}
{ V } A { N }
\end{verbatim}
(Wenn V gilt, dann A ausgeführt wird, gilt danach N.)


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

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

Beispiele
\begin{itemize}
\item
  $\wp(x := E, N) = N[x/E]$
\item
  $\wp(\verb|if |(B) \verb| then | C \verb| else | D, N)
  = B\wedge\wp(C,N) \vee \neg B\wedge \wp(D,N)$
\item
  Schleife \dots benötigt Invariante
\end{itemize}
(siehe Vorlesung Verifikation)


\end{slide}
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
