Differences

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

--- sav07_lecture_2 [2007/03/20 18:38]
vkuncak
+++ sav07_lecture_2 [2007/04/03 20:31] (current)
kremena.diatchka
@@ Line 248: / Line 248: @@
 What is a formal proof?
@@ Line 260: / Line 262: @@
 A set can be thought of as any collection of distinct objects considered as a whole. For example,
-<latex>
+\begin{equation*}
 \begin{array}{l}
 A = \{2,4,6\}\\
 B = \{4,5\}
 \end{array}
-</latex>
+\end{equation*}
 We can define many operations over sets such as.
-<latex>
+\begin{equation*}
 \begin{array}{l}
 A \cup B = \{ 2,4,5,6 \}\\
@@ Line 275: / Line 277: @@
 A / B = \{2,6\}
 \end{array}
-</latex>
+\end{equation*}
 The Cartesian product is a direct product of sets. Specifically, the Cartesian product of two sets X and Y, denoted X × Y, is the set of all possible ordered pairs whose first component is a member of X and whose second component is a member of Y:
-<latex>
+\begin{equation*}
 \begin{array}{l}
 A \times B = \{(a,b)| a \in A \wedge b \in B\}
 \end{array}
-</latex>
+\end{equation*}
 We will use binary relations on program states to represent the meaning of programs.
-A binary relation on set S is a subset of
+A binary relation on set S is a subset of $S \times S$.
-<latex>S \times S</latex>
-Diagonal is
-<latex>\Delta_S = \{(x,x) \mid x \in S \}</latex>
+The diagonal relation is $\Delta_S = \{(x,x) \mid x \in S \}$.
 Because relation is a set, all set operations apply.  In addition, we can introduce relation composition,
 denoted by circle
-<latex>r \circ s = \{(x,z) \mid \exists y.\ (x,y) \in r \land (y,z) \in s \}</latex>
+\begin{equation*}
+  r \circ s = \{(x,z) \mid \exists y.\ (x,y) \in r \land (y,z) \in s \}
+\end{equation*}
 Then
-<latex>r^n = r \circ \ldots \circ r \ \ \ \ \mbox{($n$ times)}</latex>
+\begin{equation*}
+r^n = r \circ \ldots \circ r \ \ \ \ \mbox{($n$ times)}
+\end{equation*}
-<latex>r^* = \Delta_S \cup r \cup r^2 \cup r^3 \cup \ldots </latex>
+\begin{equation*}
+r^* = \Delta_S \cup r \cup r^2 \cup r^3 \cup \ldots
+\end{equation*}
-Sets and properties are interchangable.
+Sets and predicates are interchangable.
 $x \in P$ turns set into predicate.
@@ Line 312: / Line 315: @@
 $\{ x \mid P(x)\}$ turns predicate into a set.
-<latex>
+\begin{equation*}
 \{  x \mid P_1(x) \} \cap \{ x \mid P_2(x) \}  = \{ x \mid P_1(x) \land P_2(x) \}
-</latex>
+\end{equation*}
-<latex>
+\begin{equation*}
 (x \in S_1 \cap S_2) \leftrightarrow (x \in S_1 \land x \in S_2)
-</latex>
+\end{equation*}
 Here we present few properties of transition relation
@@ Line 329: / Line 332: @@
 The property that $(r^* \circ s^*)^* = (r \cup s)^*$ is also true about composition of variables.
 ===== Programs as relations =====
@@ Line 371: / Line 372: @@
 <latex>
 \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 \}
 \end{array}
@@ Line 387: / Line 388: @@
 Accumulation of equalities.
 ===== Guarded command language =====
@@ Line 439: / Line 432: @@
 \begin{array}{ll}
 \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}
 </latex>
@@ Line 513: / Line 506: @@
 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}}.