Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_2 [2007/03/20 18:42] vkuncak |
sav07_lecture_2 [2007/03/22 20:32] vkuncak |
||
---|---|---|---|
Line 387: | Line 387: | ||
Accumulation of equalities. | Accumulation of equalities. | ||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
===== Guarded command language ===== | ===== Guarded command language ===== | ||
Line 439: | Line 431: | ||
\begin{array}{ll} | \begin{array}{ll} | ||
\llbracket havoc(x) \rrbracket = \{(s,s1)| \forall "y"\\ | \llbracket havoc(x) \rrbracket = \{(s,s1)| \forall "y"\\ | ||
- | "y" \neq "x" , s("y") = s("y")\} & \textrm { Modify a variable randomly.} | + | "y" \neq "x" , s1("y") = s("y")\} & \textrm { Modify a variable randomly.} |
\end{array} | \end{array} | ||
</latex> | </latex> | ||
Line 513: | Line 505: | ||
Weakest preconditions of assignments make wp very appealing. | Weakest preconditions of assignments make wp very appealing. | ||
- | |||
- | |||
- | |||
- | |||
- | |||
- | ===== Proving validity of linear arithmetic formulas ===== | ||
- | |||
- | Quantifier-Free Presburger arithmetic | ||
- | |||
- | <latex> | ||
- | \begin{array}{l} | ||
- | \land, \lor, \lnot, \\ | ||
- | x + y, K \cdot x, x < y, x=y | ||
- | \end{array} | ||
- | </latex> | ||
- | |||
- | Validity versus satisfiability. For all possible values of integers. | ||
- | |||
- | Reduction to integer linear programming. | ||
- | |||
- | Small model property. | ||
- | |||
- | See, for example, {{papadimitriou81complexityintegerprogramming.pdf|paper by Papadimitriou}}. | ||
- | |||
- | If we know more about the structure of solutions, we can take advantage of it as in | ||
- | {{seshiabryant04decidingquantifierfreepresburgerformulas.pdf|the paper by Seshia and Bryant}}. | ||
- | |||
Line 590: | Line 555: | ||
left, right - uninterpreted functions (can have any value, depending on the program, unlike arithmetic functions such as +,-,* that have fixed interpretation). | left, right - uninterpreted functions (can have any value, depending on the program, unlike arithmetic functions such as +,-,* that have fixed interpretation). | ||
- | ===== Reasoning about uninterpreted function symbols ===== | ||
- | |||
- | Essentially: quantifier-free first-order logic with equality. | ||
- | What are properties of equality? | ||
- | Congruence closure algorithm. Here is {{nelsonoppen80decisionprocedurescongruenceclosure.pdf|the original paper by Nelson and Oppen}}. |