LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:analyses_based_on_formulas [2009/04/08 10:39]
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 107: Line 107:
 If there is no solution, there is no invariant **of that particular template form**. If there is no solution, there is no invariant **of that particular template form**.
  
-Note: for non-numerical domains, we obtain different kinds of constraints. ​ A popular class are set constraints.+Note: for non-numerical domains, we obtain different kinds of constraints. ​ A popular class are [[sav08:​lecture25|set constraints]].
  
 ===== References ===== ===== References =====
  
   * [[Calculus of Computation Textbook]], Chapter 12   * [[Calculus of Computation Textbook]], Chapter 12
-  * [[:​sav07_lecture_7]]+