Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:interval_analysis_and_widening [2008/05/20 19:53] vkuncak |
sav08:interval_analysis_and_widening [2008/05/20 20:34] vkuncak |
||
|---|---|---|---|
| Line 40: | Line 40: | ||
| \] | \] | ||
| - | Another approach: iterate a few times with $H_i$ only (without using $w$), if not a fixpoint at this program point, then widen. | + | Approaches: |
| - | * This is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint | + | * always apply widening (we will assume this) |
| + | * iterate a few times with $H_i$ only (without using $w$), if not a fixpoint at this program point, then widen. | ||
| + | * this is not monotonic: if you start at fixpoint, it converges, if start below, can jump over fixpoint | ||
| Standard iteration: $\bot, \ldots, (F^{\#})^n(\bot), \ldots$ | Standard iteration: $\bot, \ldots, (F^{\#})^n(\bot), \ldots$ | ||
| + | |||
| Widening: $\bot, \ldots, ((W \circ F)^{\#})^n(\bot), \ldots$ | Widening: $\bot, \ldots, ((W \circ F)^{\#})^n(\bot), \ldots$ | ||
| - | Narrowing: apply fixpoint iteration after widening to improve precision. | ||
| - | Why will narrowing improve the result? | + | Here, $x \sqsubseteq W(x)$ for all $x$ by definition of $W$ |
| + | |||
| + | Narrowing: after finding fixpoint of $(W \circ F)^{\#}$, apply $F^{\#}$ to improve precision. | ||
| + | |||
| + | Observation: if $F^{\#}$ and $W$ are $\omega$-continuous functions and $x \sqsubseteq W(x)$ for all $x$, then narrowing will improve the result, that is, if $x_* = lfp (F^{\#})$ and $y_* = lfp (W \circ F^{\#})$, then $x_* \sqsubseteq y_*$ and | ||
| + | \[ | ||
| + | x_* = F(x_*) \sqsubseteq F^{\#}(y_*) \sqsubseteq (W \circ F^{\#})(y_*) \sqsubseteq y_* | ||
| + | \] | ||