\documentclass[a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{fullpage}
\setlength{\topmargin}{0mm}
\usepackage{amsmath,amssymb,stmaryrd}
\usepackage{enumitem}
\setlist[enumerate,1]{label={\alph*)}}
\usepackage[retainorgcmds]{IEEEtrantools}
\usepackage{tikz}
\definecolor{utblue}{RGB}{000,089,163}
\definecolor{utsilv}{RGB}{143,143,143}
\definecolor{utgray}{RGB}{230,230,230}
\usetikzlibrary{arrows,automata}
\tikzset{
  every picture/.style={>=stealth',shorten >=1pt,node distance=2cm,auto},
  every state/.style={scale=0.50,draw=utblue,thick,fill=utgray},
  every edge/.append style={text=utblue},
  start/.style={state,initial above,initial text=,},
  starl/.style={state,initial left,initial text=,},
  stop/.style={state,accepting below},
  stopr/.style={state,accepting right}
}

\newcommand{\banana}[1]{\llparenthesis\,{#1}\,\rrparenthesis}
\newcommand{\While}{{\mathrel{\mathsf{while}}\>}}
\newcommand{\Do}{\mathrel{\mathsf{do}}}
\newcommand{\true}{\ensuremath{\mathit{true}}}
\newcommand{\false}{\ensuremath{\mathit{false}}}
\newcommand{\imp}{\to}
\newcommand{\sequ}{\mathrel{;}}
\newcommand{\assume}[1]{\ensuremath{{#1}\,?}}
\newcommand{\assert}[1]{\ensuremath{ {#1} \, !}}
\newcommand{\havoc}[1]{\ensuremath{\mathsf{havoc}\,{#1}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Solutions for the Oral Exam (r1)}
\author{Your Name}
  
\begin{document}

\maketitle

\section{Hoare Logic}

We use the invariant $?$ to construct a proof tableaux: 
\begin{IEEEeqnarray*}{l}
    \quad \banana{x < y} \\
    \quad \banana{?} \\
  \While x < y \Do \{ \\
  \qquad 
    \begin{IEEEeqnarraybox}{l}\IEEEstrut
        \quad \banana{?} \\
        \quad \banana{?} \\
      x = x + 1 \sequ\\
        \quad \banana{?} \\
      y = y - 1 \\
        \quad \banana{?}
    \end{IEEEeqnarraybox} \\
  \} \\
    \quad \banana{?} \\
    \quad \banana{(x = y) \vee (x = y + 1}
\end{IEEEeqnarray*}


\section{VC Generation}
  
%There are a few blanks here to fill in. They are on a separate line.
The flow-graph:
\begin{center}
  \begin{tikzpicture}[node distance=35mm]
    \node[starl] (1) {$1$};
    \node[state] (2) [right of=1] {$2$};
    \node[state] (3) [right of=2] {$3$};
    \node[state] (4) [below right of=3]  {$4$};
    \node[state] (7) [below of=4]  {$7$};
    \node[state] (8) [right of=7]  {$8$};
    \node[state] (9) [right of=8]  {$9$};
    \node[state] (5) [above of=9] {$5$};
    \node[stopr] (6) [above right of=5] {$6$};

    \path[->] 
    (1) edge node [below=3mm] 
        {$?$} (2) 
    (2) edge node [above=3mm,text width=15mm] {$\havoc x \sequ \havoc y$} (3) 
    (3) edge node [rotate=45,right=1mm] 
        {$?$} (4) 
    (4) edge node [above=1mm] {$\assume{x \geq y}$} (5) 
    (4) edge node [left] {$\assume{x < y}$} (7) 
    (7) edge node [below=3mm,text width=20mm,xshift=-3mm] {$x = x + 1 \sequ y = y - 1$} (8) 
    (8) edge node [below=3mm,xshift=3mm] 
        {$?$} (9) 
    (5) edge node [right,yshift=-2mm] {$\assert{(x = y) \vee (x = y+1)}$} (6) 
    (9) edge node [right] {$\assume{\false}$} (5) 
    ;
  \end{tikzpicture}
\end{center}

The weakest preconditions at each program point $\phi_p$:
\begin{align*}
  \phi_6 &\equiv \true \\
  \phi_5 &\equiv ? \\
  \phi_9 &\equiv ? \\
  \phi_8 &\equiv ? \\
  \phi_7 &\equiv ? \\
  \phi_4 &\equiv ? \\
  \phi_3 &\equiv ? \\
  \phi_2 &\equiv ? \\
  \phi_1 &\equiv ? \\
\end{align*}

The full verification condition is
\begin{multline*}
  ?
\end{multline*}


\section{Interval Analysis}
  \begin{enumerate}
  \item $[0,0]; [0,1]; [0,2]; [0,3]; [0,4]; [0,5]; \checkmark$
  \item 
  \item 
  \item 
  \end{enumerate}
\end{document}


\section{Model-Checking}

Nothing. (See submission instructions.)
