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:39] 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 26: | ||
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) | + | \begin{array}{l} |
- | \] | + | N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ |
- | with | + | \ \ \ \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\}) |
- | \[ | + | \end{array} |
- | \bigwedge (\{C_1, \ldots, C_n \} \cap \{D_1, \ldots, D_m\}) | + | |
\] | \] | ||
Why are there no infinite chains when using such $N$ ? | Why are there no infinite chains when using such $N$ ? | ||
- | 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): |
+ | \[ | ||
+ | \begin{array}{l} | ||
+ | N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | ||
+ | \ \ \ \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\})) | ||
+ | \end{array} | ||
+ | \] | ||
+ | where | ||
+ | \[ | ||
+ | conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \} | ||
+ | \] | ||
+ | where $U$ is some class of useful formulas. | ||
=== References === | === References === |