Differences

This shows you the differences between two versions of the page.

--- sav08:analyses_based_on_formulas [2009/04/08 01:19]
vkuncak
+++ sav08:analyses_based_on_formulas [2009/04/08 10:37]
vkuncak
@@ Line 5: / Line 5: @@
 ===== Fixpoint Approach =====
-Let the domain be the set of quantifier-free formulas of first-order logic, 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.++
-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
 \]
-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".
@@ Line 24: / Line 24: @@
 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.
-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\})
+\end{array}
 \]