Differences

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

--- sav07_lecture_2 [2007/03/22 20:30]
vkuncak
+++ sav07_lecture_2 [2007/03/22 20:35]
vkuncak
@@ Line 510: / Line 510: @@
-===== 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).