Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
sav07_lecture_2 [2007/03/21 20:11] vaibhav.rajan |
sav07_lecture_2 [2007/04/01 17:25] ghid.maatouk |
||
---|---|---|---|
Line 371: | Line 371: | ||
<latex> | <latex> | ||
\begin{array}{l} | \begin{array}{l} | ||
- | \exists(x_2,y_2) \{((x_1,y_1)(x_2,y_2),(x_3,y_3)),y_2=y_1 \wedge x_2 = x_1 + 3\\ | + | \exists(x_2,y_2) \{((x_1,y_1)(x_2,y_2),(x_3,y_3)),y_2=y_1 \wedge x_2 = y_1 + 3\\ |
\wedge y_3 = y_2 \wedge x_3 = x_2 + y_2 \} | \wedge y_3 = y_2 \wedge x_3 = x_2 + y_2 \} | ||
\end{array} | \end{array} | ||
Line 505: | 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}}. | ||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | |||
- | ===== Semantics of references and arrays ===== | ||
- | |||
- | Program with class declaration | ||
- | |||
- | <code java> | ||
- | class Node { | ||
- | Node left, right; | ||
- | } | ||
- | </code> | ||
- | |||
- | How can we represent fields? | ||
- | |||
- | Possible mathematical model: fields as functions from objects to objects. | ||
- | |||
- | left : Node => Node | ||
- | right : Node => Node | ||
- | |||
- | What is the meaning of assignment? | ||
- | |||
- | x.f = y | ||
- | |||
- | <latex> | ||
- | f[x \mapsto y](z) = \left\{ \begin{array}{lr} | ||
- | y, & z=x \\ | ||
- | f(z), & z \neq x | ||
- | \end{array}\right. | ||
- | </latex> | ||
- | |||
- | Eliminating function updates in formulas. | ||
- | |||
- | Representing arrays. | ||
- | |||
- | What does this mean for our formulas? | ||
- | |||
- | <code java> | ||
- | assume (x.f = 1); | ||
- | y.f = 0; | ||
- | assert (x.f > 0) | ||
- | </code> | ||
- | |||
- | 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}}. |