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:analyses_based_on_formulas [2009/04/08 01:20] vkuncak |
sav08:analyses_based_on_formulas [2009/04/08 10:37] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
\] | \] | ||
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". | 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 ==== | ==== Approximation ==== | ||
Line 23: | Line 25: | ||
where $N$ is some approximation function. This is analogous to [[Abstract interpretation recipe]]. | where $N$ is some approximation function. This is analogous to [[Abstract interpretation recipe]]. | ||
- | Here the goal of $N$ is to ensure termination (and efficiency). | + | 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. | One generic approch: use a syntactic widening. | ||
- | View formula as a conjunction. Then approximate | + | View formula as a conjunction. Then define |
- | \[ | + | |
- | (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) | + | |
- | \] | + | |
- | with | + | |
\[ | \[ | ||
- | \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\}) | + | \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} | ||
\] | \] | ||