Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:octagons_and_relational_analysis [2008/05/20 16:23] vkuncak created |
sav08:octagons_and_relational_analysis [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Octagons and Relational Analyses ====== | ====== Octagons and Relational Analyses ====== | ||
- | * [[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|Octagons paper]] contains motivation for relational analysis | + | Intervals track possible values for each variable independently. |
+ | |||
+ | More complex analyses are //relational//: they track relations between different variables. | ||
+ | |||
+ | Example of usefulness: prove $Y \le 11$ in this program: | ||
+ | |||
+ | <code> | ||
+ | X := 10 | ||
+ | Y := 0 | ||
+ | while X >= 0 { | ||
+ | X := X-1 | ||
+ | if random() { Y = Y+1 } | ||
+ | } | ||
+ | </code> | ||
+ | |||
+ | What would interval analysis compute? At iteration $k$, we have $X \in [10-k,10]$, $Y \in [0,k]$. Although $X \in [0,10]$ stabilizes, the interval for $Y$ does not converge. We must widen and obtain $[0,+\infty]$. | ||
+ | |||
+ | What loop invariant does proof of $Y \le 11$ need? ++|$X + Y \le 10$. Note it relates values of $X$ and $Y$, interval analysis cannot compute it. ++ | ||
+ | |||
+ | Note: relational analyses can also track //changes// of variables. If we automatically insert at the beginning of each procedure | ||
+ | |||
+ | x0 = x | ||
+ | |||
+ | for each variable x, then tracking relation between x0 and x tracks the changes to x since the beginning of procedure. | ||
+ | |||
+ | Example: $x0 \le x$ means the value only increases. | ||
+ | |||
+ | ===== Octagon Domain ===== | ||
+ | |||
+ | For each pair of variables $X$, $Y$, potentially track constraints of the form | ||
+ | \begin{equation*} | ||
+ | \pm X \pm Y \le c | ||
+ | \end{equation*} | ||
+ | for some constant $c$. | ||
+ | |||
+ | It is a simpler and more efficient version of //polyhedral domain//, where constraints are general systems of linear equations of the form $A \vec x \le \vec b$ for some matrix $A$ and vector $\vec b$. | ||
+ | |||
+ | Polyhedral domain uses the theory of linear arithmetic, whereas octagon domain uses theory of //different logic//, which is simpler and allows operations to be implemented using graph algorithms. | ||
+ | |||
+ | ===== Reference ===== | ||
+ | |||
+ | * [[http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf|A. Mine: The Octagon Abstract Domain]] (has 90 pages but is easy to read) | ||