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/03/21 20:11]
vaibhav.rajan
@@ Line 248: / Line 248: @@
 What is a formal proof?
@@ Line 260: / Line 261: @@
 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 276: @@
 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.
@@ Line 312: / Line 314: @@
 $\{ 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 331: @@
 The property that $(r^* \circ s^*)^* = (r \cup s)^*$ is also true about composition of variables.
 ===== Programs as relations =====
@@ Line 387: / Line 387: @@
 Accumulation of equalities.
 ===== Guarded command language =====
@@ Line 439: / Line 431: @@
 \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>