\documentclass[a4paper,twoside,12pt]{article}
%\usepackage [reqno] {amsmath}
\usepackage{amsfonts,amstext}
\usepackage{amsmath}
\usepackage{german}
\usepackage{fullpage}
\usepackage{MnSymbol}

\newcommand{\ZETTELNUMMER}{6}
\newcommand{\ABGABEDATUM}{bis zum 30. Mai 2017, in der Vorlesung}

\newcounter{AUFGNR}
\setcounter{AUFGNR}{1}
\newcommand{\AUFGABE}[2]{\vspace{0.3cm}\item[Aufgabe~\arabic{AUFGNR}]\stepcounter{AUFGNR} #1\hfill\emph{#2}}


\newcommand{\floor}[1]{\left\lfloor{#1}\right\rfloor}
\newcommand{\ceil}[1]{\left\lceil{#1}\right\rceil}
\newcommand{\N}{\mathbb{N}}
\newcommand{\half}[1]{\frac{#1}{2}}



\renewcommand{\labelenumi}{(\alph{enumi})}
\renewcommand{\labelenumii}{(\roman{enumii})}


\begin{document}
\pagestyle{empty}
\hrule\medskip
\rule{0ex}{0ex}\\[-1ex]
\ZETTELNUMMER. Aufgabenblatt zur Vorlesung

\smallskip
\noindent
\large
\textbf{Semantik von Programmiersprachen}\hfill SoSe 2017 \\[0.5ex]
\normalsize
Wolfgang Mulzer, Max Willert

\medskip\hrule

\smallskip
\noindent
\textbf{Abgabe} \ABGABEDATUM

\vskip 0.5cm

\begin{description}

\AUFGABE{Semantische \"Aquivalenz}{10 Punkte}

\begin{enumerate}
  \item Zeigen Sie, dass die Anweisungen
    $(S_1; S_2); S_3$ und 
   $S_1; (S_2; S_3)$ semantisch \"aquivalent in 
   der strukturellen operationellen Semantik sind.

\emph{Hinweis}: Wahrscheinlich ben\"otigen Sie das 
Ergebnis von Aufgabe 5.3.

  \item Seien $S_1$ und $S_2$ zwei Anweisungen.
  Gilt dann, dass $S_1$ und $S_2$ genau dann semantisch \"aquivalent 
  in der nat\"urlichen Semantik sind, wenn
  $\mathcal{S}_\text{ns}\lsem S_1 \rsem(\sigma) = 
   \mathcal{S}_\text{ns}\lsem S_2 \rsem(\sigma)$ f\"ur alle
   Zust\"ande $\sigma$ ist?

  Begr\"unden Sie Ihre Antwort sowohl 
  anhand der allgemeinen Definitionen als auch anhand des 
  konkreten Fallbeispiels \texttt{while}.

  \item Seien $S_1$ und $S_2$ zwei Anweisungen.
  Gilt dann, dass $S_1$ und $S_2$ genau dann semantisch \"aquivalent 
  in der strukturellen Semantik sind, wenn
  $\mathcal{S}_\text{sos}\lsem S_1 \rsem(\sigma) = 
   \mathcal{S}_\text{sos}\lsem S_2 \rsem(\sigma)$ f\"ur alle
   Zust\"ande $\sigma$ ist?

  Begr\"unden Sie Ihre Antwort sowohl 
  anhand der allgemeinen Definitionen als auch anhand des 
  konkreten Fallbeispiels \texttt{while}.

\end{enumerate}


\AUFGABE{Strukturelle und nat\"urliche operationelle Semantik}{10 Punkte}

Beweisen Sie den zweiten Teil der \"Aquivalenz 
zwischen struktureller und nat\"urlicher operationeller
Semantik. Das hei\ss{}t, zeigen Sie, dass f\"ur alle 
Anweisungen $S$, Zust\"ande $\sigma$ und
$\sigma'$ und $k \in \N$ gilt:
Falls $\langle S, \sigma \rangle \Rightarrow^k \sigma'$ ist,
so auch $\langle S, \sigma \rangle \rightarrow \sigma'$.

\emph{Hinweis}: F\"uhren Sie den Beweis durch Induktion nach $k$.
Wahrscheinlich ben\"otigen Sie das Ergebnis von Aufgabe 5.3.

\newpage
\AUFGABE{Parallelit\"at}{10 Punkte}

Wir erweitern die Sprache \texttt{while} um die M\"oglichkeit der
parallelen Ausf\"uhrung. Konkret gibt es nun eine neue
Anweisung der Form $S_1 \texttt{ par } S_2$, die es erlaubt,
$S_1$ und $S_2$ parallel auszuf\"uhren.
Die strukturelle Semantik der Anweisung wird durch die folgenden
Schlussregeln definiert:
\[
\begin{array}{c}
  \langle S_1, \sigma \rangle \Rightarrow  \langle S_1', \sigma'\rangle
  \\
  \hline
  \langle S_1 \texttt{ par } S_2, \sigma\rangle \Rightarrow 
  \langle S_1' \texttt{ par } S_2, \sigma'\rangle
\end{array}
\]
\[
\begin{array}{c}
  \langle S_1, \sigma \rangle \Rightarrow  \sigma'
  \\
  \hline
  \langle S_1 \texttt{ par } S_2, \sigma\rangle \Rightarrow 
  \langle S_2, \sigma'\rangle
\end{array}
\]
\[
\begin{array}{c}
  \langle S_2, \sigma \rangle \Rightarrow  \langle S_2', \sigma'\rangle
  \\
  \hline
  \langle S_1 \texttt{ par } S_2, \sigma\rangle \Rightarrow 
  \langle S_1 \texttt{ par } S_2', \sigma'\rangle
\end{array}
\]
\[
\begin{array}{c}
  \langle S_2, \sigma \rangle \Rightarrow  \sigma'
  \\
  \hline
  \langle S_1 \texttt{ par } S_2, \sigma\rangle \Rightarrow 
  \langle S_1, \sigma'\rangle
\end{array}
\]
\begin{enumerate}
\item Jetzt ist die strukturelle
Semantik nicht mehr determiniert. Geben Sie ein Beispiel f\"ur eine
Anweisung und einen Startzustand, aus denen sich zwei verschiedene
Endzust\"ande ableiten lassen.
\item Versuchen Sie, die Anweisung $S_1 \texttt{ par } S_2$ in 
der nat\"urlichen Semantik zu formulieren. Welche Probleme ergeben
sich?  
\item Vergleichen Sie die strukturelle und die nat\"urliche
operationelle Semantik hinsichtlich ihrer Vor- und Nachteile.
\item (\emph{freiwillig, 5 Zusatzpunkte})
Betrachten Sie die Anweisung $\texttt{protect } S \texttt{ end}$,
welches einen \emph{kritischen Abschnitt} definiert. 
Das bedeutet, dass die Anweisung $S$ \emph{atomar} ausgef\"uhrt 
wird und es zu keiner parallelen Verschr\"ankung kommen darf.
Modellieren Sie $\texttt{protect } S \texttt{ end}$ in der strukturellen
operationellen Semantik und verdeutlichen Sie Ihre Definition
anhand eines sinnvollen Beispiels. 
\end{enumerate}
\end{description}
\end{document}
