\begin{slide}{Denotationale Semantik (I)}

vereinfachtes Modell, 
damit Eigenschaften entscheidbar werden
(sind die Programme $P_1, P_2$ äquivalent?)

Syntax: Programme 
\begin{itemize}\itemsep 0pt
\item Aktionen,
\item Zustandsprädikate (in Tests)
\item Sequenz/Block, if, goto/while.
\end{itemize}

Beispiel:
\begin{verbatim}
while (B && !C) { P; if (C) Q; }
\end{verbatim}
\end{slide}

\begin{slide}{Denotationale Semantik (II)} 
\parskip 0pt
Semantik des Programms $P$ ist 
  Menge der Spuren von $P$.
  \begin{itemize}\itemsep 0pt\parskip 2pt
\item \emph{Spur} $=$ eine Folge von Paaren
  von Zustand und Aktion,
\item ein \emph{Zustand}
  ist eine Belegung der Prädikatsymbole,
\item jede Aktion zerstört 
  alle Zustandsinformation.
\end{itemize}

Satz: Diese Spursprachen 
(von goto- und while-Programmen)
sind \emph{regulär}. 

Beweis: Konstruktion über endlichen Automaten.
\begin{itemize} \itemsep 0pt\parskip 2pt
\item Zustandsmenge $=$ Prädikatbelegungen $\times$ Anweisungs-Nummer
\item Transitionen? (Beispiele)
\end{itemize}

Damit ist Spur-Äquivalenz von Programmen entscheidbar.\\
Beziehung zu tatsächlicher Äquivalenz?

\end{slide}

