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

\newcommand{\ZETTELNUMMER}{12}
\newcommand{\ABGABEDATUM}{bis zum 11. 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 vorletzte Aufgabenblatt.
\vskip 0.5cm

\begin{description}

\AUFGABE{Stetigkeit}{15 Punkte}

\begin{enumerate}
    \item Sei $p : \mathbf{State} \rightarrow \mathbb{B}$ ein
      Pr\"adikat und $g: \mathbf{State} \rightarrow \mathbf{State}$
      beliebig. Zeigen Sie, dass
      das Funktional 
      $F_1: (\mathbf{State} \rightarrow \mathbf{State})
        \rightarrow (\mathbf{State} \rightarrow \mathbf{State})$
	mit $F_1(f) = \cond(p, g, f)$ stetig ist.
    \item Sei $g: \mathbf{State} \rightarrow \mathbf{State}$
      beliebig. Zeigen Sie, dass
      das Funktional 
      $F_2: (\mathbf{State} \rightarrow \mathbf{State})
        \rightarrow (\mathbf{State} \rightarrow \mathbf{State})$
	mit $F_2(f) = g \circ f$ stetig ist.
    \item Sei $g: \mathbf{State} \rightarrow \mathbf{State}$
      beliebig. Zeigen Sie, dass
      das Funktional 
      $F_3: (\mathbf{State} \rightarrow \mathbf{State})
        \rightarrow (\mathbf{State} \rightarrow \mathbf{State})$
	mit $F_3(f) = f \circ g$ stetig ist.
\end{enumerate}

\AUFGABE{Bestimmung der Zustands\"uberf\"uhrungsfunktion}{10 Punkte}

Bestimmen Sie folgenden Zustands\"uberf\"uhrungsfunktionen anhand
der Definitionen:
\begin{enumerate}
  \item $\mathcal{S}_\text{ds}\lsem \texttt{while true do skip} \rsem$.
  \item $\mathcal{S}_\text{ds}\lsem 
  \texttt{z := 0; while y <= x do (z := z + 1; x := x - y)} \rsem$.
\end{enumerate}

\AUFGABE{Repeat-Until}{5 Punkte}

Erweitern Sie die Sprache \texttt{while} um eine
\texttt{repeat}-\texttt{until} Schleife. Definieren
Sie die denotationalle Semantik, und zeigen Sie, dass
Ihre semantische Funktion wohldefiniert ist.

Ihre Definitionen sollen unabh\"angig von der Existenz einer 
\texttt{while}-Schleife in der Sprache sein.
\end{description}
\end{document}
