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

\newcommand{\ZETTELNUMMER}{4}
\newcommand{\ABGABEDATUM}{bis zum 15. Mai 2017, 12 Uhr, in den
Briefkasten neben Raum 111}

\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{\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{Repeat-Until}{10 Punkte}

\begin{enumerate}
\item
Erweitern Sie die Sprache \texttt{while} um eine
\texttt{repeat}-\texttt{until} Schleife. Definieren
Sie die nat\"urliche Semantik durch geeignete Schlussregeln.

Ihre Definitionen sollen unabh\"angig von der Existenz einer 
\texttt{while}-Schleife in der Sprache sein.
\item
Zeigen Sie: Die Anweisungen
\texttt{repeat $S$ until $b$} und 
\texttt{$S$; if $b$ then skip else (repeat $S$ until $b$)}
sind semantisch \"aquivalent.
\end{enumerate}

\AUFGABE{Terminierung von Anweisungen}{10 Punkte}

Sei $S$ eine Anweisung. Wir sagen
$S$ \emph{terminiert immer}, falls es
f\"ur alle Zust\"ande $\sigma$ einen Zustand
$\sigma'$ gibt mit $\langle S, \sigma \rangle \rightarrow \sigma'$.
Wir sagen $S$ \emph{terminiert nie}, falls es
f\"ur keinen Zustand $\sigma$ einen Zustand 
$\sigma'$ gibt mit $\langle S, \sigma \rangle \rightarrow \sigma'$

Welche der folgenden Anweisungen terminieren immer? Welche terminieren
nie? Begr\"unden Sie Ihre Antworten anhand der Axiome und Schlussregeln
f\"ur die nat\"urliche Semantik.

\begin{enumerate}
  \item \text{while $\neg$ (x=1) do (y := y*x; x := x - 1)}
  \item \text{while 1 $\leq$ x do (y := y*x; x := x - 1)}
  \item \text{while true do skip}
\end{enumerate}

\AUFGABE{Implementierung in Haskell}{10 Punkte}

Implementieren Sie die nat\"urliche Semantik von \texttt{while}
in Haskell.

\end{description}
\end{document}
