- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

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