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

\newcommand{\ZETTELNUMMER}{8}
\newcommand{\ABGABEDATUM}{bis zum 13. 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{\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{Unterprogramme mit dynamischem G\"ultigkeitsbereich}{18 Punkte}

\begin{enumerate}
\item
Sei $\sigma$ ein Zustand mit $\sigma(\texttt{x}) = 2$.
Konstruieren Sie einen Ableitungsbaum f\"ur
$\langle S, \sigma \rangle$, wobei $S$ die 
folgende Anweisung ist:
\begin{verbatim}
begin 
    proc fac is 
    begin 
        var z := x;
        if x = 1 then 
            skip
        else
            x := x - 1;
            call fac;
            y := z * y
    end;
    y := 1;
    call fac
end
\end{verbatim}
\item
Benutzen Sie die Schlussregeln aus der Vorlesung, um
den Wert von \texttt{y} in der vorvorletzten Zeile 
bei der Ausf\"uhrung der folgenden Anweisung zu ermitteln.
\begin{verbatim}
begin 
    var x := 0;
    proc p is
        x := x * 2;
    proc q is
        call p;
    begin 
        var x := 5;
        proc p is 
            x := x + 1;
        call q;
        y := x
    end
end
\end{verbatim}
\end{enumerate}

\newpage
\AUFGABE{Unterprogramme mit statischem G\"ultigkeitsbereich}{8 Punkte}

In dieser Aufgabe wollen wir eine Semantik f\"ur Unterprogramme
definieren, so dass die Bezeichner der Unterprogramme sich
auf den \emph{statischen} G\"ultigkeitsbereich beziehen.

\begin{enumerate}
    \item Wir definieren den lokalen Kontext so um, dass wir mit
       jedem Bezeichner f\"ur ein Unterprogramm nun auch den
       lokalen Kontext zum Zeitpunkt der Definition des Unterprogramms
       speichern:
       \[
         \mathbf{Env}_P = \mathbf{Pname} \rightarrow \mathbf{Stm} 
       \times \mathbf{Env}_P.
       \]
       Definieren Sie die Funktion 
       $\text{akt}_P: \mathbf{D}_P \times \mathbf{Env}_P
         \rightarrow \mathbf{Env}_P$
      so um, dass nun auch die lokalen Kontexte gespeichert werden.
    \item Geben Sie eine neue Schlussregel $[\text{call}_\text{ns}]$
      f\"ur Unterprogrammaufrufe, welche den lokalen Kontext
      des jeweiligen Unterprogramms verwendet.
      Beachten Sie dabei den Fall von rekursiven Unterprogrammen.
    \item Illustrieren Sie Ihre Definitionen anhand eines einfachen
      Beispiels.
\end{enumerate}

\AUFGABE{Fixpunkte}{4 Punkte}

Betrachten Sie die Anweisung
$\texttt{while } \neg (\texttt{x} = 0) \text{ do skip}$.

\begin{enumerate}
  \item Geben Sie eine kurze Definition des
    zugeh\"origen Funktionals 
    \[ F(f) = \text{cond}(\mathcal{B}\lsem b \rsem, f \circ
    \mathcal{S}_\text{ds} \lsem S \rsem , \text{id}).\]
  \item Betrachten Sie die Funktion $g: \mathbf{State} \rightarrow 
  \mathbf{State}$ definiert durch 
  $g(\sigma) = \perp$, falls $\sigma(\texttt{x}) \neq 0$ ist,  und
  $g(\sigma) = \sigma$, sonst.
  Zeigen Sie, dass $g$ ein Fixpunkt des Funktionals $F$ aus (a) ist.
\end{enumerate}
\end{description}
\end{document}
