Differences
This shows you the differences between two versions of the page.
sav08:octagons_and_relational_analysis [2008/05/20 23:56] vkuncak |
sav08:octagons_and_relational_analysis [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Octagons and Relational Analyses ====== | ||
- | |||
- | 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 | ||
- | \[ | ||
- | \pm X \pm Y \le c | ||
- | \] | ||
- | 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|Octagons paper]] has 90 pages but is easy to read | ||