\begin{slide}{Dynamische Semantik}

\begin{itemize}
\item
  operational:

  beschreibt Wirkung von Anweisungen 
  durch Änderung des Programmzustandes
\item
  denotational:

  ordnet jedem (Teil-)Programm einen Wert zu,
  Bsp: eine Funktion (höherer Ordnung).

  Beweis von Programmeigenschaften durch
  Term-Umformungen
\item
  axiomatisch (Bsp: Hoare-Kalkül):

  enthält Schlußregeln, 
  um Aussagen über Programme zu beweisen
\end{itemize}

\end{slide}

