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

\newcommand{\ZETTELNUMMER}{7}
\newcommand{\ABGABEDATUM}{bis zum 6. Juni 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{Zusicherungen}{10 Punkte}

Erweitern Sie \texttt{while} um
das neue Sprachkonstrukt $\texttt{assert } b \texttt{ before } S$.
Wenn die Boolesche Bedingung $b$ erf\"ullt ist, so wird die Anweisung 
$S$ ausgef\"uhrt,
ansonsten wird das Programm abgebrochen.

\begin{enumerate}
\item Erweitern Sie die strukturelle operationelle Semantik,
um die Zusicherungen zu modellieren (verwenden Sie dabei nicht
die Anweisung \texttt{abort}).
\item Geben Sie ein Beispielprogramm, das Zusicherungen verwendet.
Illustrieren Sie seinen Ablauf mit zwei Ableitungsfolgen.
\item
Zeigen Sie: $\texttt{assert true before }S$ ist semantisch
\"aquivalent zu $S$. 
\item Ist $\texttt{assert false before }S$ semantisch \"aquivalent
zu \texttt{while true do skip}? Zu
\texttt{skip}?
\end{enumerate}

\AUFGABE{Nichtdeterminismus}{10 Punkte}

Erweitern Sie \texttt{while} um Nichtdeterminismus.
Nun gibt es eine neue Anweisung $S_1 \texttt{ or } S_2$,
mit der das Programm nichtdeterministisch entweder die
Anweisung $S_1$ ausf\"uhren kann oder die Anweisung $S_2$
ausf\"uhren kann.

\begin{enumerate}
\item
  Erweitern Sie die nat\"urliche operationelle Semantik um
  Schlussregeln f\"ur die Anweisung $S_1 \texttt{ or } S_2$.
\item
  Erweitern Sie die strukturelle operationelle Semantik um
  Schlussregeln f\"ur die Anweisung $S_1 \texttt{ or } S_2$.
\item
  Ist 
  $x\texttt{ := }1$ semantisch \"aquivalent zu 
  $x\texttt{ := }1\texttt{ or }(\texttt{while true do skip})$ in der nat\"urlichen
  operationellen Semantik?
  Wie ist es in der strukturellen operationellen Semantik?

\end{enumerate}

\AUFGABE{Bl\"ocke}{10 Punkte}

Erweitern Sie Ihre Haskell-Implementierung von \texttt{while},
so dass sie Bl\"ocke unterst\"utzt.
Erl\"autern Sie Ihren Quelltext durch geeignete Kommentare und
f\"uhren Sie sinnvolle Testl\"aufe durch.
\end{description}
\end{document}
