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]] | + | |