\begin{frame}
  \frametitle{Verification-Condition Generation}

  Given:
  \begin{itemize}
  \item program and
  \item specification
  \end{itemize}
  how to express program correctness
  as a \textbf{verification condition}, \\
  a formula implying that program satisfies the specification?

  \pause

  \
  
  How to implement verification condition generation as an algorithm?    

  \pause

  \

  Example program that verifies in Stainless:
  
  \lstinputlisting{example.scala}

\end{frame}

\begin{frame}
\frametitle{Programs are Formulas. Specifications are Formulas}

A program fragment can be represented by a formula relating initial and final state. Consider a program with variables $x, y$
\[
\begin{array}{rc}
\mbox{program:} & x = x + 2; y = x + 10 \\
\mbox{relation:} & \{ ((x,y),(x',y')) \mid x' = x + 2 \land y' = x + 12 \} \\
\mbox{formula:} & \hspace*{2cm} x' = x + 2 \land y' = x + 12 
\end{array}
\]
Specification was: $old(this).x > 0 \rightarrow (x > 2 \land y > 12)$

We express that program satisfies the postcondition using \textbf{relation subset}:
\[
\begin{array}{rl}
          & \{ ((x,y),(x',y')) \mid x' = x + 2 \land y' = x + 12 \}  \\
\subseteq & \{ ((x,y),(x',y')) \mid x > 0 \rightarrow (x' > 2 \land y' > 12) \}
\end{array}
\]
which reduces to the \textbf{validity of the following implication}:
\[
\begin{array}{rl}
            & x' = x + 2 \land y' = x + 12 \\
\rightarrow & (x > 0 \rightarrow (x' > 2 \land y' > 12))
\end{array}
\]

\end{frame}


\begin{frame}
\frametitle{Simple Imperative Programs}
 $F$ - formulas, $t$ - terms (with only pure mathematical operations) 

 Fixed number of mutable variables $V = \{x_1,\ldots,x_n\}$

 Imperative statements:
 \begin{itemize}
 \item $\mathbf{x=t}$: change $x \in V$ to have value given by $t$; leave vars in $V \setminus \{x\}$ unchanged
 \item $\mathbf{if(F) c_1\ else\ c_2}$: if $F$ holds, execute $c_1$ else execute $c_2$
 \item $\mathbf{c_1; c_2}$: first execute $c_1$, then execute $c_2$
 \end{itemize}
 Statements for introducing and restricting non-determinism:
 \begin{itemize}
 \item $\mathbf{havoc(x)}$: non-deterministically change $x \in V$ to have an arbitrary value; leave vars in $V \setminus \{x\}$ unchanged
 \item $\mathbf{if(*)\ c_1\ else\ c_2}$: arbitrarily choose to run $c_1$ or $c_2$
 \item $\mathbf{assume(F)}$: block all executions where $F$ does not hold
 \end{itemize}
 Given such loop-free program $c$ with conditionals, compute a polynomial-sized formula $R(c)$ of form:
 $\exists \bar z. F(\bar x, \bar z, \bar x')$ describing relation between 
 initial values of variables $x_1,\ldots,x_n$ and final values of variables $x'_1,\ldots,x'_n$
\end{frame}

\begin{frame}
\frametitle{Construction Formula that Describe Relations}

$c$ - imperative command

\vspace*{3cm}

$R(c)$ - formula describing relation between initial and final states of execution of $c$

\ \\

If $\rho(c)$ describes the relation, then $R(c)$ is formula such that
\[
    \rho(c) = \{ (\bar x, \bar x') \mid R(c) \}
\]
$R(c)$ is a formula between unprimed variables $\bar x$ and primed variables $\bar x'$

\end{frame}


\begin{frame}
\frametitle{Formula for Assignment}

\[
    x = t
\]
\pause
$R(x=t)$:
\[
    x' = t \land \bigwedge_{v \in V \setminus \{x\}} v' = v
\]

Note that the formula must explicitly state which variables
remain the same (here: all except $x$). Otherwise, those
variables would not be constrained by the relation, so
they could take arbitrary value in the state after the command.

\

Examples:

$R(x = x + 2) \ = \ \ x' = x + 2 \ \land\ y'=y$

$R(y = x + 10) \ = \ \ x' = x \ \land\ y'=x + 10$

\end{frame}

\begin{frame}
\frametitle{Formula for if-else}

\[
   if(b)\ c_1\ else\ c_2
\]
\pause
$R(if(b)\ c_1\ else\ c_2)$:
\[
    (b \land R(c_1)) \lor (\lnot b \land R(c_2))
\]

\end{frame}

\begin{frame}
\frametitle{Command semicolon}

\[
    c_1; c_2
\]
\pause
Corresponds to relation composition:
\[
  r_1 \circ r_2 = \{ (\bar x,\bar x') \mid \exists \bar x''. (\bar x,\bar x'') \in r_1 \land
                                                           (\bar x'',\bar x') \in r_2 \}
\]
\pause
What are $R(c_1)$ and $R(c_2)$ and in terms of which variables they are expressed?
\pause Each in terms of $\bar x$ and $\bar x'$.

Let $r_1 = \{(\bar x,\bar x')\mid R(c_1)\}$, $r_2 = \{(\bar x,\bar x')\mid R(c_2)\}$

Thus, $(\bar x,\bar x'') \in r_1 \ \longleftrightarrow\ (\bar x,\bar x'') \in \{(\bar x,\bar x')\mid R(c_1)\} \ \longleftrightarrow\ R(c_1)[\bar x':=\bar x'']$

Similarly, $(\bar x'',\bar x') \in r_2 \ \longleftrightarrow\ R(c_2)[\bar x':=\bar x'']$

\pause
$R(c_1;c_2)\ \longleftrightarrow \ (\bar x, \bar x') \in r_1 \circ r_2 \ \longleftrightarrow$
\[ \exists \bar x''.\ \ 
   R(c_1)[\bar x' := \bar x''] \land R(c_2)[\bar x := \bar x'']
\]
where $\bar x''$ are freshly picked names of intermediate states. 
\begin{itemize}
\item a useful convention: $\bar x''$ refer to position in program source code, $\bar x^{i}$
\end{itemize}

\end{frame}

\begin{frame}
  \frametitle{Computing relation for the example from before}

\[
  \begin{array}[t]{l}
  R(x = x + 2; y = x + 10) \ =  \exists \bar x''.\ \ 
    R(c_1)[\bar x' := \bar x''] \land R(c_2)[\bar x := \bar x'']\relax \\[0.5ex]
    = \exists x'',y''.\ \
    \begin{array}[t]{l}
    (x' = x + 2 \ \land\ y'=y)[x':=x'',y':=y'']\relax \ \land \\
      (x' = x \ \land\ y'=x+10)[x:=x'',y:=y''] \\[0.5ex]
    \end{array} \\
    = \exists x'',y''.\ \
    \begin{array}[t]{l}
      (x'' = x + 2 \ \land\ y''=y) \ \land \\
      (x' = x'' \ \land\ y'=x''+10) \hspace*{2cm} (*) \\[0.5ex]
    \end{array} \\
    \longleftrightarrow  \ \ \
      (x' = x + 2 \ \land\ y'=x + 2 +10) \\
    \longleftrightarrow \ \ \
      (x' = x + 2 \ \land\ y'=x + 12) 
  \end{array}
\]

\

Where at step $(*)$ we used (twice) the ``one-point rule'' of logic with equality:
\[
     (\exists u. (u = t \land F)) \ \longleftrightarrow\ F[u:=t]
\]
if $u \notin FV(t)$.
\end{frame}

\begin{frame}
\frametitle{havoc}

Definition of HAVOC
\begin{enumerate}
\item wide and general destruction: devastation
\item great confusion and disorder
\end{enumerate}

Example of use: 

\ 

\ \ y = 12; havoc(x); assume(x + x = y)

\ 

ends up dividing $y$ by two and assigning result to $x$.

\

Translation, $R(havoc(x))$:
\pause
\[
    \bigwedge_{v \in V \setminus \{x\}} v' = v
\]
This again illustrates ``politically correct'' approach to describing the destruction
of values of variables: just do not mention them.

\end{frame}

\begin{frame}
\frametitle{Non-deterministic choice}
\[
   if(*)\ c_1\ else\ c_2
\]
\pause
$R(if(*)\ c_1\ else\ c_2)$:
\[
    R(c_1) \lor R(c_2)
\]

\ \\

\begin{itemize}
\item translation is simply a disjunction -- this is why construct is interesting
\item corresponds to branching in control-flow graphs
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{assume}

\[
    assume(F)
\]
\pause
$R(assume(F))$:
\[
     F \land \bigwedge_{v \in V} v' = v
\]

\begin{itemize}
\item\pause This command does not change any state.
\item\pause If $F$ does not hold, it stops with ``instantaneous success''.
\end{itemize}
\end{frame}

\newcommand{\minnum}[1]{\mbox{\tiny #1}}

\begin{frame}
\frametitle{Example of Translation}

\[
\begin{array}{l}
\minnum{0} \\
(if\ (b)\ x = x + 1\ else\ y = x + 2); \\
\minnum{1} \\
x = x + 5; \\
\minnum{2} \\
(if\ (*)\ y = y + 1\ else\ x = y) \\
\minnum{3} 
\end{array}
\]
becomes
\[
\hspace*{-1em}
\exists x_1,y_1,x_2,y_2.
\begin{array}[t]{l}
((b \land \mathbf{x_1 = x + 1} \land y_1 = y) \lor (\lnot b \land x_1 = x \land \mathbf{y_1=x+2}))  \\
\land\ (\mathbf{x_2 = x_1 + 5} \land y_2 = y_1) \\
\land\ ((x' = x_2 \land \mathbf{y' = y_2 + 1}) \lor (\mathbf{x' = y_2} \land y' = y_2))
\end{array}\]

Think of execution trace $(x_0,y_0),(x_1,y_1),(x_2,y_2),(x_3,y_3)$ where 
\begin{itemize}
\item $(x_0,y_0)$ is denoted by $(x,y)$
\item $(x_3,y_3)$ is denoted by $(x',y')$
\end{itemize}

\end{frame}

% \begin{frame}
% \frametitle{Imperative Presburger Arithmetic Programs}

% $F$ - formulas, $t$ - terms - as in functional programs so far

% Fixed number of mutable integer variables $V = \{x_1,\ldots,x_n\}$

% Imperative statements:
% \begin{itemize}
% \item $\mathbf{x=t}$: change $x \in V$ to have value given by $t$; leave vars in $V \setminus \{x\}$ unchanged
% \item $\mathbf{if(F) c_1\ else\ c_2}$: if $F$ holds, execute $c_1$ else execute $c_2$
% \item $\mathbf{c_1; c_2}$: first execute $c_1$, then execute $c_2$
% \end{itemize}
% Statements for introducing and restricting non-determinism:
% \begin{itemize}
% \item $\mathbf{havoc(x)}$: non-deterministically change $x \in V$ to have an arbitrary value; leave vars in $V \setminus \{x\}$ unchanged
% \item $\mathbf{if(*)\ c_1\ else\ c_2}$: arbitrarily choose to run $c_1$ or $c_2$
% \item $\mathbf{assume(F)}$: block all executions where $F$ does not hold
% \end{itemize}
% Given such loop-free program $c$ with conditionals, compute a polynomial-sized formula $R(c)$ of form:
% $\exists \bar z. F(\bar x, \bar z, \bar x')$ describing relation between 
% initial values of variables $x_1,\ldots,x_n$ and final values of variables $x'_1,\ldots,x'_n$
% \end{frame}

\begin{frame}
\frametitle{Justifying the name for assume(F)}

Compute and simplify as much as possible each of the following expressions:
\begin{enumerate}
\item $R(assume(F); c)$ \pause \ \ $=$ \  $F \land R(c)$
\item $R(c; assume(F))$ \pause \ \ $=$ \ $R(c) \land F[\bar x := \bar x']$ \\
where $F[\bar x := \bar x']$ denotes $F$ with all variables replaced with primed versions
\end{enumerate}

\end{frame}

\begin{frame}
\frametitle{Expressing \textbf{if} through non-deterministic choice and assume}

\pause
\lstinputlisting{ifdesugar.scala}

Indeed, apply translation to both sides and observe that generated
formulas are equivalent.

\end{frame}

\begin{frame}
\frametitle{Expressing assignment through havoc and assume}

\pause
\lstinputlisting{assignhavoc.scala}

\ \\

Under what conditions this holds?

\pause
$x \notin FV(e)$

\ \\

Illustration of the problem: $havoc(x); \ assume(x == x + 1)$

\ \\ \pause

Luckily, we can rewrite it into $x_{fresh} = x + 1; x=x_{fresh}$ 

\end{frame}

\begin{frame}
\frametitle{Loop-Free Programs as Relations: Summary}

\[\begin{array}{r|c|l}
   \mbox{command } c  & R(c) & \rho(c) \\\hline\hline
  (x=t)               & x' = t \land \bigwedge_{v \in V \setminus \{x\}} v' = v 
                      & \\
  \semic{c_1}{c_2}    & \exists \bar z.\ \ 
                         R(c_1)[\bar x' := \bar z] \land R(c_2)[\bar x := \bar z]
                      & \rho(c_1) \circ \rho(c_2) \\
  \ifstar{c_1}{c_2}  & R(c_1) \lor R(c_2) & \rho(c_1) \cup \rho(c_2) \\
  \mathbf{assume(F)} & F \land \bigwedge_{v \in V} v'=v & \Delta_{S(F)} 
\end{array}
\]

$\rho(x_i=t) = \{ ((x_1,\ldots,x_i,\ldots,x_n),(x_1,\ldots,x_i',\ldots,x_n) \mid x'_i = t \}$

$S(F) = \{ \bar x \mid F \}$, \ \ $\Delta_A = \{ (\bar x, \bar x) \mid \bar x \in A \}$
(diagonal relation on $A$)

$\Delta$ (without subscript) is identity on entire set of states (no-op)

We always have: $\rho(c) = \{ (\bar x, \bar x') \mid R(c) \}$ 

Shorthands:
\[\begin{array}{c|c}
   \ifstar{c_1}{c_2}   &  \ndchoice{c_1}{c_2}   \\\hline
   \mathbf{assume}(F) & [F] 
\end{array}\]
Examples:
\[\begin{array}{l}
  \ifcond{F}{c_1}{c_2} 
  \ \ \equiv \ \
  { [F];c_1 \ \choiceop \ [\lnot F];c_2 } \\
  \ifcondskip{F}{c}
  \ \ \equiv \ \ 
  { [F];c \ \choiceop \ [\lnot F] } \\
\end{array}\]
\end{frame}

\begin{frame}
\titleslide{Program Paths}
\end{frame}

\begin{frame}
\frametitle{Loop-Free Programs}

$c$ - a loop-free program whose assignments, havocs, and assumes are $c_1,\ldots,c_n$

\ \\

The relation $\rho(c)$ is of the form $E(\rho(c_1),\ldots,\rho(c_n))$; 
it composes meanings of 
$c_1,\ldots,c_n$ using union ($\cup$) and composition $(\circ)$

\begin{tabular}{c|c|c}
\begin{minipage}{2.6cm}
\lstinputlisting{twoifs.scala}
\end{minipage}
&
\begin{minipage}{3.2cm}
\lstinputlisting{twoifsguard.scala}
\end{minipage}
&
\begin{minipage}{4cm}
\[\begin{array}{l}
\big( \Delta_{S(x>0)} \circ \rho(x=x-1) \\
\ \ \ \cup \\
\ \Delta_{S(\lnot(x>0))} \circ \rho(x=0) \\
\big) \circ \\
\big( \Delta_{S(y>0)} \circ \rho(y=y-1) \\
\ \ \ \cup \\
\ \Delta_{S(\lnot(y>0))} \circ \rho(y=x+1) \\
\big) 
\end{array}\]
\end{minipage}
\end{tabular}

Note: $\circ$ binds stronger than $\cup$, so $r \circ s \cup t = (r \circ s) \cup t$

\end{frame}

\begin{frame}
\frametitle{Normal Form for Loop-Free Programs}

Composition distributes through union:
\[
    (r_1 \cup r_2) \circ (s_1 \cup s_2) =
    r_1 \circ s_1 \ \cup \
    r_1 \circ s_2 \ \cup \
    r_2 \circ s_1 \ \cup \
    r_2 \circ s_2
\]

Example corresponding to two if-else statements one after another:
\begin{tabular}{ccc}
\begin{minipage}{4cm}
\[\begin{array}{l}
\big( \Delta_1 \circ r_1 \\
\ \ \ \cup \\
\ \Delta_2 \circ r_2 \\
\big) \circ \\
\big( \Delta_3 \circ r_3 \\
\ \ \ \cup \\
\ \Delta_4 \circ r_4 \\
\big) 
\end{array}\]
\end{minipage}
& 
\begin{minipage}{1cm}
\[ \equiv \]
\end{minipage}
&
\begin{minipage}{4cm}
\[\begin{array}{l}
\Delta_1 \circ r_1 \circ \Delta_3 \circ r_3 \ \cup \\
\Delta_1 \circ r_1 \circ \Delta_4 \circ r_4 \ \cup \\
\Delta_2 \circ r_2 \circ \Delta_3 \circ r_3 \ \cup \\
\Delta_2 \circ r_2 \circ \Delta_4 \circ r_4 
\end{array}\]
\end{minipage}
\end{tabular}

Sequential composition of basic statements is called basic path.

Loop-free code describes finitely many (exponentially many) paths.

\end{frame}
