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 [2008/05/21 10:21] vkuncak |
sav08:analyses_based_on_formulas [2009/04/08 10:37] vkuncak |
||
---|---|---|---|
Line 5: | Line 5: | ||
===== Fixpoint Approach ===== | ===== Fixpoint Approach ===== | ||
- | Let the domain be the set of formulas, ordered by implication | + | 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.++ | 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. | + | 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 | \bigvee_{i=1}^{\infty} y = i x | ||
\] | \] | ||
- | In general, a logic that can represent exact limits 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 24: | ||
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 | + | |
\[ | \[ | ||
+ | \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\}) | \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\}) | ||
+ | \end{array} | ||
\] | \] | ||
Line 39: | Line 43: | ||
To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set). | To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set). | ||
+ | |||
+ | === 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 ===== | ===== Constraint-Based Approach ===== |