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

\newcommand{\ZETTELNUMMER}{13}
\newcommand{\ABGABEDATUM}{bis zum 18. Juli 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{\half}[1]{\frac{#1}{2}}
\newcommand{\N}{\mathbb{N}}


\DeclareMathOperator{\FIX}{FIX}
\DeclareMathOperator{\cond}{cond}

\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

\noindent
Dies ist das letzte Aufgabenblatt.
\vskip 0.5cm

\begin{description}

\AUFGABE{Denotationelle und nat\"urliche Semantik}{15 Punkte}

Zeigen Sie \emph{direkt}, also ohne Umweg \"uber die
strukturelle  Semantik, dass f\"ur alle Anweisungen
$S$ von \texttt{while} gilt:
$\mathcal{S}_\text{ds}\lsem S \rsem =
\mathcal{S}_\text{ns} \lsem S \rsem$.

\AUFGABE{Z\"ahlschleifen}{15 Punkte}

Erweitern Sie \texttt{while} um die Anweisung
\texttt{for $x$ := $a_1$ to $a_2$ do $S$},
welche eine Z\"ahlschleife darstellt.

Modellieren Sie Z\"ahlschleifen in der
nat\"urlichen operationellen Semantik,
der strukturellen operationellen Semantik
und in der denotationellen Semantik.
Greifen  Sie dabei nicht auf die Existenz einer
\texttt{while}-Schleife zur\"uck.

Werten Sie dann die jeweiligen semantischen Funktionen
auf der Anweisung 
\begin{verbatim}
  y := 1; for z := 1 to x do (y := y * x;  x := x - 1)
\end{verbatim}
auf einem Zustand $\sigma$ mit $\sigma(\texttt{x}) = 3$ aus.

\emph{Hinweis}: Sie d\"urfen eine Funktion 
   $\mathcal{N}^{-1}: \N \rightarrow \Sigma^*$
  verwenden, welche jeder nat\"urlichen Zahl eine 
  Darstellung in der Syntax von \texttt{while} zuordnet.
\end{description}
\end{document}
