\begin{frame}
\titleslide{Properties of Program Contexts}
\end{frame}

\begin{frame}
\frametitle{Some Properties of Relations}

$
   (p_1 \subseteq p_2) \rightarrow (p_1 \circ p) \subseteq (p_2 \circ p)
$

\vfill

$
   (p_1 \subseteq p_2) \rightarrow (p \circ p_1) \subseteq (p \circ p_2)
$

\vfill

$
   (p_1 \subseteq p_2) \land (q_1 \subseteq q_2) \ \ \rightarrow\ \
   (p_1 \cup q_1) \subseteq (p_2 \cup q_2) 
$

\vfill

$
   (p_1 \cup p_2) \circ q = (p_1 \circ q) \cup (p_2 \circ q)
$

\vfill

\end{frame}


\begin{frame}
\frametitle{Monotonicity of Expressions using $\cup$ and $\circ$}

%For a program with $k$ integer variables, $S = \mathbb{Z}^k$

Consider relations that are subsets of $S \times S$ (i.e. $S^2$)

The set of all such relations is
\[
   C = \{ r \mid r \subseteq S^2 \}
\]

Let $E(r)$ be given by any expression built from relation $r$
and some additional relations $b_1,\ldots,b_n$, using $\cup$ and $\circ$.

Example: $E(r) = (b_1 \circ r) \cup (r \circ b_2)$

$E(r)$ is function $C \to C$, maps relations to relations

\textbf{Claim:}
$E$ is monotonic function on $C$:
\[
   r_1 \subseteq r_2 \rightarrow E(r_1) \subseteq E(r_2)
\]
Prove of disprove.

\pause
Proof: induction on the expression tree defining $E$, using monotonicity properties of $\cup$ and $\circ$

\end{frame}

\begin{frame}
\frametitle{Union-Distributivity of Expressions using $\cup$ and $\circ$}

Claim: $E$ distributes over unions, that is, if $r_i, i \in I$ is a family of relations,
\[
   E(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E(r_i)
\]
Prove or disprove.

\pause
False. Take $E(r) = r \circ r$ and consider relations $r_1, r_2$. The claim becomes
\[
    (r_1 \cup r_2) \circ (r_1 \cup r_2) = r_1 \circ r_1 \cup r_2 \circ r_2
\]
that is,
\[
    r_1 {\circ} r_1 \cup r_1 {\circ} r_2 \cup r_2 {\circ} r_1 \cup r_2 {\circ} r_2 
  = r_1 {\circ} r_1 \cup r_2 {\circ} r_2
\]
Taking, for example, $r_1 = \{(1,2)\}$, $r_2 = \{ (2,3)\}$ we obtain 
\[
    \{ (1,3) \} = \emptyset \ \ \ \ \alert{(false)}
\]

\end{frame}

\begin{frame}
\frametitle{Union ``Distributivity'' in One Direction}

Lemma:
\[
   E(\bigcup_{i \in I} r_i) \supseteq \bigcup_{i \in I} E(r_i)
\]
\pause
Proof.
Let $r = \bigcup_{i \in I} r_i$.
Note that, for every $i$, $r_i \subseteq r$. We have shown that $E$ is monotonic,
so $E(r_i) \subseteq E(r)$. Since all $E(r_i)$ are included in $E(r)$, so is their union, so
\[
   \bigcup E(r_i) \subseteq E(r)
\]
as desired.

\end{frame}

\begin{frame}
\frametitle{Union-Distributivity - Refined}

Does distributivity
\[
   E(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E(r_i)
\]
hold, for each of these cases
\begin{enumerate}
\item If $E(r)$ is given by an expression containing $r$ at most once?
\pause Proof: Induction on expression for $E(r)$. Only one branch of the tree may contain $r$. Note
previous counter-example uses $r$ twice.

\pause
\item If $E(r)$ contains $r$ any number of times, but $I$ is a set of natural numbers
and $r_i$ is an increasing sequence:
$r_1 \subseteq r_2 \subseteq r_3 \subseteq \ldots$
\pause Induction. In the previous counter-example the largest relation will contain all other $r_i \circ r_j$.

\item If $E(r)$ contains $r$ any number of times, but $r_i, i \in I$ is a 
\textbf{directed family} of relations: for each $i,j$ there exists $k$ such that
$r_i \cup r_j \subseteq r_k$, and $I$ is possibly uncountably infinite.
\pause Induction. Generalizes the previous case.

\end{enumerate}
\end{frame}

\begin{frame}
  \frametitle{Union-Distributivity Case of Increasing Sequence}

  \[
   E(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E(r_i)
 \]
 for $I = \{ 1,2,\ldots\}$ and $r_1 \subseteq r_2 \subseteq \ldots$

 Proof is by induction on the structure of the tree for
 expression $E(r)$ using monotonicity property. Case $E(r) = E_1(r) \circ E_2(r)$,
 assuming by inductive hypothesis
 $E_1(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E_1(r_i)$
 and
 $E_2(\bigcup_{i \in I} r_i) = \bigcup_{i \in I} E_2(r_i)$.

  Let $r = \bigcup_{i \in I} r_i$.
  We know by previous monotonicity argument that
  $\bigcup_{i \in I} E(r_i) \subseteq E(\bigcup_{i \in I} r_i)$,
  so we just need to show the converse direction. Let
  $(x,x') \in E(r)$ be arbitrary. We need to show $(x,x') \in \bigcup_{i \in I} E(r_i)$.
  Since $(x,x') \in E_1(r) \circ E_2(r)$, there exists $z$ such that
  $(x,z) \in E_1(r)$ and $(z,x') \in E_2(r)$. By inductive hypothesis,
  $(x,z) \in \bigcup_{i\in I} E_1(r_i)$ and
  $(z,x') \in \bigcup_{i\in I} E_2(r_i)$. By definition of union there exists $i_1,i_2$ such that
  $(x,z) \in E_1(r_{i_1})$ and $(z,x') \in E_2(r_{i_2})$. Let $j = max(i_1,i_2)$. Then
  $r_{i_1} \subseteq r_j$ and  $r_{i_2} \subseteq r_j$, so, by monotonicity of $E_1$ and $E_2$,
  $(x,z) \in E_1(r_j)$ and $(z,x') \in E_2(r_j)$. Thus, $(x,x') \in E_1(r_j) \circ E_2(r_j) = E(r_j)$
  so $(x,x') \in \bigcup_{i \in I} E(r_i)$ as desired.
\end{frame}

% =========================================================
\begin{frame}

  \vfill
\centerline{\huge More on Mapping Code to Formulas}
  \vfill
  
\end{frame}

\begin{frame}
\frametitle{Local Mutable Variables}

Assume our global variables are $V = \{ x, z \}$

Program $P$ introduces a local variable $y$ inside a nested block:
\[
   x = x + 1; \{ \mathbf{var}\ y; y = x + 3; z = x + y + z \}; x = x + z
\]
$R(P)$ should be a relation between $(x,z)$ and $(x',z')$. 

Each statement should be relation between variables in scope. Inside the block
we have variables $V_1 = \{ x, y, z \}$. For assignment statement $c$: \ \ \ \
$
  z = x + y + z
$, \\
$R(c)$ is a relation between $x,y,z$ and $x',y',z'$.

Convention: consider the initial values of variables to be arbitrary

$R(y = x + 3; z = x + y + z) = $  
 \pause 
 $y' = x + 3 \land z' = 2x + 3 + z \land x' = x$

\ \\

\pause
$R(\{ \mathbf{var}\ y; y = x + 3; z = x + y + z\}){=} $ \
 \pause 
 $z' = 2x + 3 + z \land x' = x$

\end{frame}

\begin{frame}
\frametitle{Local Variable Translation}

$R_V(P)$ is formula for $P$ in the scope that has the set of variables $V$. For example,
\[
   R_V(x=t)\ = \ x' = t \land \bigwedge_{v \in V \setminus \{x\}} v' = v
\]

Then define

$R_V(\{ var\ y; P \}) \ = \ $ \pause $\exists y,y'. R_{V \cup \{y\}}(P)$

\ \\

\pause

Example: $R_{\{x,y,z\}}(x = y + 1) = (x' = y + 1 \land y'=y \land z = z')$, so
\[
    R_{\{x,z\}}(\{var\ y; x = y + 1\}) \ \ = \ \ \exists y,y'.\ x' = y + 1 \land y'=y \land z = z'
\]
In the last formula we can eliminate $y'$ (the result is that $y'=y$ disappears) and then eliminate
$y$ from $x'=y+1$ i.e. $y=x'-1$ (over integers). Thus the formula is equivalent to $z=z'$.

\pause
Exercise: express havoc(x) using var.
\pause
\[
   R_V(havoc(x))\ \iff \  R_V(\{ var\ y;\ x = y \})
\]
%\pause
%Exercise: give transformation that lifts all variables to be global

\end{frame}

