% \documentclass{beamer}
% \usepackage[utf8]{inputenc}
% \usepackage{amsthm}
% \usepackage{amssymb}
% \usepackage{wasysym}
% \usepackage{listings}
% \input{../common/scalalistings}

% \input{../common/mysymbols}
% \input{../common/mywords-en}
% \input{../common/constructors}

% \setbeamersize{text margin left=0.3cm, text margin right=0.3cm}

% \usepackage{pgf}
% \usepackage{tikz}
% \usetikzlibrary{arrows,automata,fit}

% \title{Lecturecise 17 \\ Predicate Abstraction. Predicate Discovery}
% \date{2013}

% \beamertemplatenavigationsymbolsempty

% \begin{document}

% \maketitle

\begin{frame}{Predicate Abstraction}
Abstract interpretation domain is determined by a set of formulas (predicates) ${\cal P}$ on program
variables. 

Example: ${\cal P} = \{ P_0, P_1, P_2, P_3 \}$ where
\[
\begin{array}{rcl}
P_0 &\equiv& \mbox{false} \\
P_1 &\equiv& 0 < x \\
P_2 &\equiv& 0 < y \\
P_3 &\equiv& x < y \\
\end{array}
\]
Analysis tries to construct invariants from these predicates using 
\begin{itemize}
\item conjunctions, e.g. $P_1 \land P_3$
\item more generally, conjunctions and disjunctions, e.g. $P_3 \land (P_1 \lor P_2)$
\end{itemize}
\pause
For now: we consider only conjunctions. 

We assume $P_0 \equiv \mbox{false}$, other predicates in ${\cal P}$ are arbitrary
\begin{itemize}
\item expressed in a logic for which we have a theorem prover
\end{itemize}

\end{frame}

\begin{frame}{Example of Analysis Result}

\[
    {\cal P} = \{ false, 0<x, 0<=x, 0<y, x<y, x=0, y=1, x<1000,1000 \le x \}
\]

\lstinputlisting{example1.scala}

\end{frame}

\begin{frame}{Lattice of Conjunctions of Predicates and Concretization}

${\cal P} = \{ P_0,P_1,\ldots, P_n \}$ - predicates 
\begin{itemize}
\item formulas whose free variables denote program variables
\end{itemize}

$A = 2^{\cal P}$, so for $a \in A$ we have $a \subseteq {\cal P}$

Example: $a_0 = \{ 0 < x, x < y \}$.

$s \models F$ means: formula $F$ is true for variables given by the program state $s$
\[
  \gamma(a) = \{ s \mid s \models \bigwedge_{P \in a} P \}
\]
Shorthand: $\bigwedge a$ means $\bigwedge_{P \in a} P$

Example: $\gamma(a_0) = \pause \{ s \mid s \models 0 < x \land x < y \}$. \pause
We often assume states are pairs $(x,y)$. Then
$\gamma(a_0) = \pause \{ (x,y) \mid 0 < x \land x < y \}$.

\pause
If $a_1 \subseteq a_2$ then $\bigwedge a_2$ implies $\bigwedge a_1$, so $\gamma(a_2) \subseteq \gamma(a_1)$.

\pause
Define:
\[
     a_1 \sqsubseteq a_2 \ \  \iff \ \ a_2 \subseteq a_1
\]
Lemma: $a_1 \sqsubseteq a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$

\pause Does the converse hold?
\end{frame}

\begin{frame}{Size of the Lattice}

\[
    \{ false, 0 < x, x < y \} \sqsubseteq \{ 0 < x, 0 < y \} \sqsubseteq \{ 0 < x \} \sqsubseteq \emptyset
\]

Draw the Hasse diagram for the lattice $(A,\sqsubseteq)$ i.e. $(2^{\cal P}, \supseteq)$ for
${\cal P} = \{ P_0,P_1,P_2 \}$ a three-element set.

\vspace*{4cm}

\pause What is the top and what is the bottom element of this lattice?

\pause What is the height of the lattice?

\pause What is the height of such lattice when ${\cal P} = \{P_0,P_1,\ldots,P_n\}$?

\pause Do $\sqcup$ and $\sqcap$ exist?
\end{frame}

\begin{frame}{Galois Connection}

For $\gamma(a) = \{ s \mid s \models \bigwedge_{P \in a} P \}$ we define
\[
   \alpha(c) = \{ P \in {\cal P} \mid \forall s \in c.\ s \models P \}
\]

\[\begin{array}{rcl}
   \alpha(\{(-1,1)\}) &=& \pause \{ y > 0 \} \\
   \pause \alpha(\{(1,1), (2,2), (3,6) \}) &=& \pause \{ x > 0, y > 0 \} \\
   \pause \alpha(\{(1,0), (0,1) \}) &=& \pause \emptyset \\
   \pause \gamma(\emptyset) & = & \pause S \mbox{ (set of all states, empty conjunction) }
\end{array}\]

Is $(\alpha,\gamma)$ a Galois connection between $(A,\sqsubseteq)$ and $(C,\subseteq)$?

\end{frame}

\begin{frame}{Galois Connection for Predicate Abstraction}

We show $(\alpha,\gamma)$ is a Galois Connection. We need to show that
\[
    c \subseteq \gamma(a) \ \iff\  \alpha(c) \supseteq a
\]

\pause But both conditions easily reduce to
\[
    \forall P \in a.\ \forall s \in c.\ s \models P
\]

\pause
Shorthand: in logic, if $M$ is a set of assignments to variables (structures) and ${\cal A}$ is
a set of formulas (e.g. axioms), then $M \models {\cal A}$ means 
\[
   \forall m \in M. \forall F \in {\cal A}.\  m \models F
\]
So, both conditions of Galois connection reduce to $c \models a$

\end{frame}

\begin{frame}{Not a Galois Insertion}

Is it the case that $\alpha(\gamma(a))=a$?

\pause
We show this is not the case. This is because $\gamma$ is not injective.

Indeed, take $a_1 = \{false\}$ and $a_2 = \{false, x > 0\}$. Then
\[
   \gamma(a_1) = \emptyset = \gamma(a_2)
\]
Note $\alpha(\gamma(a_1)) = \alpha({\cal P}) = \alpha(\gamma(a_2))$, but $a_1 \neq a_2$, but it is not the case
that $a_1 = a_2$. In this particular case,
\[
    \alpha(\emptyset) = {\cal P}
\]
and $a_1 \neq {\cal P}$ so
\[
    \alpha(\gamma(a_1)) \neq a_1
\]
\pause
However, the approach works and is sound, even without the condition $\alpha(\gamma(a))=a$.

\pause
Can you find an example of non-injectivity in our 4 predicates that does not involve false?
\end{frame}

\begin{frame}{Monotonicity of $\alpha$}

Let $c_1 \subseteq c_2$.

We wish to prove that $\alpha(c_1) \supseteq \alpha(c_2)$. 

\pause Let $P \in \alpha(c_2)$. Then for all $(x,y) \in c_2$ we have $P(x,y)$.

\pause Then also for all $(x,y) \in c_1$ we have $P(x,y)$, because $c_1 \subseteq c_2$.

\pause Therefore $P \in \alpha(c_1)$. We showed $c_2 \subseteq c_1$, so $c_1 \sqsubseteq c_2$.

\end{frame}

\begin{frame}{Computing Approximate Strongest Postcondition}

${\cal P} = \{ false, 0 < x, 0 < y, x < y \}$

Consider computing $sp^\#(\{0<x\},y:=x+1)$. We can test for each predicate $P' \in {\cal P}$ whether
\[
    x > 0 \land (y' = x + 1 \land x'=x) \implies P'(x',y')
\]
We obtain that the condition holds for $0<x$, $0<y$, and for $x < y$, but not for $false$. Thus,
\[
   sp^\#(\{0<x\},y:=x+1) = \{ 0 < x, 0 < y, x < y \}
\]
Compute
\[\begin{array}{l}
   sp^\#(\{0<x\},y:=x-1) = \pause \{ 0 < x \} \\
   \pause sp^\#(\{0<x,x<y\},x:=x-1) = \pause \{ 0 < y, x < y \}
\end{array}
\]
\pause
What is the relation between $\{0<x,x<y\}$ and $\{0<x,0<y,x<y\}$?

\end{frame}

\begin{frame}{Deriving Rule for Computing sp}
\small
Fix some command given by relation $r$. 

Denote $a' = sp^\#(a,r)$. We are computing $a'$. For correctness we need 
\[
   sp(\gamma(a),r) \subseteq \gamma(a')
\]
Thanks to Galois connection, this is equivalent to
\[
   \alpha(sp(\gamma(a),r)) \sqsubseteq a'
\]
We wish to find the smallest lattice element $a'$, which is the largest set (this gives the tightest approximation). So we let
\[
   a' = \alpha(sp(\gamma(a),r))
\]
Given that $\gamma(a) = \{ s \mid s \models \bigwedge a \}$, and
$\alpha(c) = \{ P \in {\cal P} \mid \forall s \in c.\ s \models P \}$,
\[
   a'  = \{ P' \in {\cal P} \mid \forall (x',y') \in sp(\gamma(a),r).\ P'(x',y') \} 
\]
\end{frame}

\begin{frame}{Continuing the Derivation of sp}
\[
   a'  = \{ P' \in {\cal P} \mid \forall (x',y'). 
(x',y') \in sp(\gamma(a),r) \rightarrow P'(x',y') \} 
\]
Let $R(x,y,x',y')$ denote the meaning of relation $r$

\pause
Then $(x',y') \in sp(\gamma(a),r)$ means
\[
   \exists x,y. (x,y) \in \gamma(a) \land R(x,y,x',y')
\]
which, after expanding $\gamma$, gives
\[
   \exists x,y. (\bigwedge_{P\in a} P(x,y)) \land R(x,y,x',y')
\]
We then plug this expression back into $a'$ definition.
Because the existentials are left of implication, the result is:
\[
    a' = \{ P' \in {\cal P} \mid   \forall x,y,x'y'.\
      (\bigwedge_{P\in a} P(x,y)) \land R(x,y,x',y') \rightarrow P'(x',y') \}
\]
\end{frame}

\begin{frame}{Example of Analysis Result}

\[
    {\cal P} = \{ false, 0<x, 0<=x, 0<y, x<y, x=0, y=1, x<1000,1000 \le x \}
\]

\lstinputlisting{example1.scala}

\end{frame}

\begin{frame}{Formulation in terms of Removing Predicates}

At program entry: $\top$, which is: \pause $\emptyset$ of predicates

At all other points: $\bot$, which is: \pause the set of all predicates ${\cal P}$

Lattice elements grow in CFG $\leadsto$ the set of predicates decrease

\pause We remove predicates that do not hold
\end{frame}

% \begin{frame}{Limitations of Conjunctions}

% \lstinputlisting{example2.scala}

% \end{frame}

% \begin{frame}{Disjunctive Analysis}

% Disjunction of conjunctions.

% Sets of sets.

% $\alpha$ and $\gamma$

% Approximations: apply per disjunct.

% Powerdomain. Power and cost of powerdomains.

% \end{frame}

% \begin{frame}{Reachability tree}
% \end{frame}

% \begin{frame}{Path Feasibility Checking}

% \end{frame}

% \begin{frame}{Adding Predicates to Remove Infeasible Paths}

% Adding weakest preconditions

% Adding strongest postconditions

% Increasing the power of generalization:
% \begin{itemize}
% \item do not add complex formulas, but their parts
% \item no need to add sp or wp, but anything that forms a sufficiently annotated Hoare proof that this path is infeasible
% \end{itemize}

% \end{frame}

%\end{document}
