Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:analyses_based_on_formulas [2009/04/08 10:44] vkuncak |
sav08:analyses_based_on_formulas [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 10: | Line 10: | ||
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 | 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 | ||
- | \[ | + | \begin{equation*} |
\bigvee_{i=1}^{\infty} y = i x | \bigvee_{i=1}^{\infty} y = i x | ||
- | \] | + | \end{equation*} |
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". | ||
Line 21: | Line 21: | ||
Rule for computing formula (called 'fact') in step $k+1$ at program point $p'$ | Rule for computing formula (called 'fact') in step $k+1$ at program point $p'$ | ||
- | \[ | + | \begin{equation*} |
\mbox{fact}^{k+1}(p') := N\left(\mbox{fact}^k(p) \vee \bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}^k(p),r(p,p'))\right) | \mbox{fact}^{k+1}(p') := N\left(\mbox{fact}^k(p) \vee \bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}^k(p),r(p,p'))\right) | ||
- | \] | + | \end{equation*} |
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). The essential condition is that | Here the goal of $N$ is to ensure termination (and efficiency). The essential condition is that | ||
- | \[ | + | \begin{equation*} |
F \rightarrow N(F) | F \rightarrow N(F) | ||
- | \] | + | \end{equation*} |
is a valid formula. | is a valid formula. | ||
Line 35: | Line 35: | ||
View formula as a conjunction. Then define | View formula as a conjunction. Then define | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | 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} | \end{array} | ||
- | \] | + | \end{equation*} |
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{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
N\left( (C_1 \land \ldots \land C_n) \lor (D_1 \land \ldots \land D_m) \right) = \\ | 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\})) | \ \ \ \bigwedge (conseq(\{C_1, \ldots, C_n \}) \cap conseq(\{D_1, \ldots, D_m\})) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
where | where | ||
- | \[ | + | \begin{equation*} |
conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \} | conseq(S) = \{ F \in U.\ \ (S \rightarrow F) \mbox{ is valid } \} | ||
- | \] | + | \end{equation*} |
where $U$ is some class of useful formulas. | where $U$ is some class of useful formulas. | ||
Line 68: | Line 68: | ||
Search for //any// fixpoint - it will be a set of loop invariants: | Search for //any// fixpoint - it will be a set of loop invariants: | ||
- | \[ | + | \begin{equation*} |
\left(\bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}(p),r(p,p'))\right) \rightarrow \mbox{fact}(p) | \left(\bigvee_{(p,p') \in E} sp^{\#}(\mbox{fact}(p),r(p,p'))\right) \rightarrow \mbox{fact}(p) | ||
- | \] | + | \end{equation*} |
Works better if we also have postconditions and assertions that need to be satisfied (otherwise we may come up with trivial invariants). | Works better if we also have postconditions and assertions that need to be satisfied (otherwise we may come up with trivial invariants). | ||
Line 91: | Line 91: | ||
Invariant of the form $a_1 X + a_2 Y = a_0$. | Invariant of the form $a_1 X + a_2 Y = a_0$. | ||
- | \[ | + | \begin{equation*} |
X=10 \land Y = 0 \rightarrow a_1 X + a_2 Y = a_0 | X=10 \land Y = 0 \rightarrow a_1 X + a_2 Y = a_0 | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 Y = a_0 | a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 Y = a_0 | ||
- | \] | + | \end{equation*} |
- | \[ | + | \begin{equation*} |
a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 (Y+1) = a_0 | a_1 X + a_2 Y = a_0 \land X \ge 0 \rightarrow a_1 (X-1) + a_2 (Y+1) = a_0 | ||
- | \] | + | \end{equation*} |
Such equations need to hold for all values of $X$,$Y$, which gives constraints on $a_0,a_1,a_2$ that can be solved based on properties of real fields (linear programming, Farkas lemma). | Such equations need to hold for all values of $X$,$Y$, which gives constraints on $a_0,a_1,a_2$ that can be solved based on properties of real fields (linear programming, Farkas lemma). | ||
Line 112: | Line 112: | ||
* [[Calculus of Computation Textbook]], Chapter 12 | * [[Calculus of Computation Textbook]], Chapter 12 | ||
- | * [[:sav07_lecture_7]] | + |