Differences

This shows you the differences between two versions of the page.

--- sav08:abstract_interpretation [2008/04/29 23:22]
vkuncak created
+++ sav08:abstract_interpretation [2008/04/30 11:02]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Abstract Interpretation ======
-[[:sav07_lecture_6#Abstract interpretation]]
+Goal: Invariant Inference by Approximation ======
+Approximate strongest postcondition $sp$ with operator $sp\#$ whose fixedpoint e.g. has a finite height.
+Let PS denote program states and $C = 2^{PS}$ denote the set of all subsets of PS, so $S \subseteq PS$ and $S \in C$ for a set of states S.  We introduce an abstract analysis domain A and functions
+\begin{equation*}
+\begin{array}{l}
+  \gamma : A \to C \ \ \mbox{concretization function} \\
+\end{array}
+\end{equation*}
+Instead of working with C, we work with simpler domain A, which is the data structure for analysis.
+Examples of A:
+  * mapping from variables to information about the values they can have (interval analysis, sign analysis, constant propagation)
+  * formula F (usually in canonical form) such that $\gamma(F) = \{ x. F \}$
+So, we will impose that our domain is partial order.  It is useful to require additional property, namely that we have lattice, which have "union"-like and "intersection"-like operations.
+Note that $\gamma$ allows us to define set-like operations on A that correspond to operations on A:
+\begin{equation*}
+  a_1 \sqsubseteq a_2   \iff   \gamma(a_1) \subseteq \gamma(a_2)
+\end{equation*}
+Instead of $sp : C \to C$, we have its approximation $sp\# : A \to A$.  To be sound we need to have
+\begin{equation*}
+  \gamma(sp\#(a_1,r)) \supseteq sp(\gamma(a_1),r)
+\end{equation*}
+This is the most important condition for abstract interpretation.
+One way to find $sp\#$ it is to have $\alpha$ that goes the other way
+\begin{equation*}
+\begin{array}{l}
+  \alpha : C \to A \ \ \mbox{abstraction function}
+\end{array}
+\end{equation*}
+such that
+\begin{equation*}
+\begin{array}{l}
+   \gamma(\alpha(S)) \supseteq S \\
+   \alpha(\gamma(a)) = a
+\end{array}
+\end{equation*}
+Then we can write a definition of $sp\# : A \to A$ in terms of it:
+\begin{equation*}
+  sp\#(a,r) = \alpha(sp(\gamma(a),r))
+\end{equation*}
+and we call this "the best transformer".
+==== Abstract computation of program semantics ====
+In our lattice we have
+\begin{eqnarray*}
+  \gamma(a_1 \sqcup a_2) &\supseteq& \gamma(a_1) \cup \gamma(a_2)
+\end{eqnarray*}
+because of the way we defined order.
+Consider first only a single loop.
+Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$.  We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop):
+\begin{equation*}
+  sp\#(a,r^*) = a \sqcup sp\#(sp\#(a,r),r^*)
+\end{equation*}
+We can then iterate this equation until it stabilizes.
+From the properties of $\gamma$ it follows that the result is approximation of the set of reachable states.
+When does it stabilize?  Note that the sequence is increasing and if we ever repeat we have stabilized.  If there are no infinite ascending chains, the computation terminates.
+==== References ====
+  * [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|A Tutorial Abstract Interpretation by the inventor Patrick Cousot]]
+  * [[:sav07_lecture_7|Approximation Expressed Using Formulas]]
+  * [[Calculus of Computation Textbook]], Chapter 12 on invariant generation