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

\newcommand{\ZETTELNUMMER}{5}
\newcommand{\ABGABEDATUM}{bis zum 23. 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{Die nat\"urliche Semantik ist determiniert}{10 Punkte}

Die nat\"urliche Semantik von \texttt{while} ist determiniert.
Das hei\ss{}t, f\"ur alle Anweisungen $S$ und f\"ur alle
Zust\"ande $\sigma$, $\sigma_1$ und $\sigma_2$ gilt:
\[
(\langle S, \sigma\rangle \rightarrow \sigma_1 \wedge
\langle S, \sigma\rangle \rightarrow \sigma_2) \Rightarrow
\sigma_1 = \sigma_2.
\]
Beweisen Sie dies durch Induktion nach der Tiefe des
Ableitungsbaums von $\langle S, \sigma\rangle \rightarrow \sigma_1$.

\AUFGABE{Repeat-Until}{10 Punkte}
\begin{enumerate}
\item
Erweitern Sie die Sprache \texttt{while} um eine
\texttt{repeat}-\texttt{until} Schleife. Definieren
Sie die strukturelle Semantik durch geeignete Schlussregeln.

Ihre Definitionen sollen unabh\"angig von der Existenz einer 
\texttt{while}-Schleife in der Sprache sein.
\item
Sei $\sigma$ ein Zustand mit $\sigma(x) = 3$.
Geben Sie die  Ableitungsfolge f\"ur die
Anweisung
\begin{verbatim}
  y := 1; repeat y := y*x; x := x - 1; until x = 1
\end{verbatim}
an. Begr\"unden Sie die einzelnen Schritte.
\end{enumerate}

\AUFGABE{Eigenschaften der strukturellen operationellen Semantik}{10 Punkte}

Entscheiden Sie f\"ur die beiden folgenden Aussagen, 
ob sie wahr oder falsch sind. Geben Sie jeweils einen Beweis
oder ein Gegenbeispiel.

\begin{enumerate}
  \item F\"ur alle Anweisungen $S_1$, $S_2$ 
  und alle Zust\"ande $\sigma$, $\sigma'$ 
  gilt: 
  \[
\text{Aus }   \langle S_1; S_2, \sigma\rangle \Rightarrow^* \langle S_2, 
   \sigma'\rangle 
    \text{ folgt }
    \langle S_1, \sigma\rangle \Rightarrow^*  \sigma'.
  \]
  \item F\"ur alle Anweisungen $S_1$, $S_2$,
  alle Zust\"ande $\sigma$, $\sigma'$ und alle $k \in \N$ 
  gilt: 
  \[
\text{Aus }   \langle S_1, \sigma\rangle \Rightarrow^k  \sigma'
    \text{ folgt }
    \langle S_1; S_2, \sigma\rangle \Rightarrow^k  \langle S_2, 
    \sigma'\rangle.
  \]

\end{enumerate}

\end{description}
\end{document}
