Differences

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

--- sav08:analyses_based_on_formulas [2009/04/08 10:44]
vkuncak
+++ sav08:analyses_based_on_formulas [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Analyses Based on Formulas ======
-Many analyses can be viewed in this way.
-===== Fixpoint Approach =====
-Let the domain be the set of quantifier-free formulas of some logic, ordered by implication
-Is this a partial order?  ++|We would need to do a quotient construction to obtain it.++
-Non-existence of limits: infinite disjunction need not be a formula of our logic, e.g. consider formulas on linear arithmetic and take the limit
-\[
-    \bigvee_{i=1}^{\infty} y = i x
-\]
-In general, a logic that can represent exact least upper bounds needs to express the conditions such as "there exists a sequence of statements that produces the given state".
-==== Approximation ====
-Rule for computing formula (called 'fact') in step $k+1$ at program point $p'$
-\[
-  \mbox{fact}^{k+1}(p') := N\left(\mbox{fact}^k(p) \vee \bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}^k(p),r(p,p'))\right)
-\]
-where $N$ is some approximation function.  This is analogous to [[Abstract interpretation recipe]].
-Here the goal of $N$ is to ensure termination (and efficiency). The essential condition is that
-\[
-    F \rightarrow N(F)
-\]
-is a valid formula.
-One generic approch: use a syntactic widening.
-View formula as a conjunction.  Then define
-\[
-\begin{array}{l}
-   N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\
-\ \ \   \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\})
-\end{array}
-\]
-Why are there no infinite chains when using such $N$ ?
-To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set):
-\[
-\begin{array}{l}
-   N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\
-\ \ \   \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\}))
-\end{array}
-\]
-where
-\[
-    conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \}
-\]
-where $U$ is some class of useful formulas.
-=== References ===
-  * [[http://citeseer.ist.psu.edu/244634.html|Safety Checking of Machine Code]] described induction iteration method (wp instead of sp)
-  * analysis based on sets in the Hob analysis system
-===== Constraint-Based Approach =====
-Give up //least// fixpoint requirement (it is approximation anyway).
-Search for //any// fixpoint - it will be a set of loop invariants:
-\[
-   \left(\bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}(p),r(p,p'))\right) \rightarrow \mbox{fact}(p)
-\]
-Works better if we also have postconditions and assertions that need to be satisfied (otherwise we may come up with trivial invariants).
-Assume a 'template' for the invariant, e.g. (Karr's analysis) each fact is a linear equation $c_1 x_1 + \ldots + c_n x_n = c_0$ on program variables $x_1,\ldots,x_n$.
-The condition for loop invariants gives a system of equations on coefficients $c_0(p),c_1(p),\ldots,c_n(p)$ for each of the finitely many program points $p$.
-If there exists a solution, this gives an invariant.
-<code>
-X := 10
-Y := 0
-while (X >= 0) {
-  X := X-1
-  if random() { Y = Y+1 }
-}
-</code>
-Invariant of the form $a_1 X + a_2 Y = a_0$.
-\[
-   X=10 \land Y = 0 \rightarrow a_1 X + a_2 Y = a_0
-\]
-\[
-   a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 Y = a_0
-\]
-\[
-   a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 (Y+1) = a_0
-\]
-Such equations need to hold for all values of $X$,$Y$, which gives constraints on $a_0,a_1,a_2$ that can be solved based on properties of real fields (linear programming, Farkas lemma).
-Thanks to quantifier elimination for real fields, the technique extends to polynomial invariants as well.
-If there is no solution, there is no invariant **of that particular template form**.
-Note: for non-numerical domains, we obtain different kinds of constraints.  A popular class are [[sav08:lecture25|set constraints]].
-===== References =====
-  * [[Calculus of Computation Textbook]], Chapter 12
-  * [[:sav07_lecture_7]]