Differences

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

@@ Line 1: / Line 1: @@
+====== Lecture 2 ======
+===== Manually proving an example =====
+Recall our example from [[SAV07 Lecture 1|Lecture 1]], with a loop invariant:
+<code Java>
+    public static int sum(int a0, int n0)
+   /*:
+     requires "a0 > 0 & n0 > 0"
+     ensures "result > 0"
+   */
+    {
+        int res = 0, a = a0, n = n0;
+        while //: inv "a > 0 & res >= 0 & (n = n0 | res > 0)"
+            (n > 0)
+        {
+            a = 2*a;
+            res = res + a;
+            n = n - 1;
+        }
+        return res;
+    }
+</code>
+What formulas do we need to prove?
+Two questions:
+  * why is this correct
+  * how do we automate it?
+To answer the first question, we first need to define semantics of programs.
+===== Logical preliminaries =====
+We used these constructs in mathematics all the time.
+Formalizing them is useful for
+  * foundation of mathematics (first half of 19th century)
+  * proving formulas automatically: need to represent formulas and make correct reasoning steps on them
+==== Propositional logic ====
+Basic propositional operations:
+<latex>
+\land, \lor, \lnot, \rightarrow, \leftrightarrow
+</latex>
+Context-free grammar for propositional logic.
+Example formula:
+<latex>
+((p \rightarrow q) \land (\lnot p \rightarrow r)) \leftrightarrow
+((p \land q) \lor (\lnot p \land r))
+</latex>
+Is "false implies true" valid formula?
+There is an algorithm that checks whether a formula is
+  * satisfiable
+  * valid
+What is the algorithm?
+SAT solvers: http://www.satlive.org/
+==== First-order logic (predicate calculus) ====
+Predicate: a function from some arguments into true or false.
+Example: "p divides q" is a binary predicate on p and q.
+Predicate calculus is concerned with properties of predicates (regardless of what these predicates are).
+Constructs in predicate calculus:
+<latex>
+\forall, \exists, P(t_1,t_2), t_3=f(t_4)
+</latex>
+Context-free grammar for first-order logic.
+Drinker's paradox (made more politically correct):
+in every restaurant there is a guest such that if this guest is having a dessert,
+then everyone in the restaurant is having a dessert.
+How to formalize it?
+Is it valid?  Why?
+Tarskian semantics for first-order logic.
+Is there an algorithm for first-order logic?
+Checking (and enumerating) proofs.
+What is a formal proof?
+==== Sets and relations ====
+Constructs
+<latex>
+\begin{array}{l}
+\{ x_1,\ldots,x_n \}  \\
+\{ x \mid P(x) \}  \\
+\in, \cap, \cup, \subseteq, \times
+\end{array}
+</latex>
+Example:
+<latex>
+\begin{array}{rcl}
+A &=& \{2,4,6\} \\
+B &=& \{3,6\}
+\end{array}
+</latex>
+We will use binary relations on program states to represent the meaning of programs.
+A binary relation on set S is a subset of
+<latex>S \times S</latex>
+Diagonal is
+<latex>\Delta_S = \{(x,x) \mid x \in S \}</latex>
+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>
+Then
+<latex>r^n = r \circ \ldots \circ r \ \ \ \ \mbox{($n$ times)}</latex>
+<latex>r^* = \Delta_S \cup r \cup r^2 \cup r^3 \cup \ldots </latex>
+Sets and properties are interchangable.
+<latex>
+x \in P
+</latex>
+turns set into predicate.
+<latex>
+\{ x \mid P(x)\}
+</latex>
+turns predicate into a set.
+<latex>
+\{ x \mid P_1(x) \} \cap \{ x \mid P_2(x) \}  = \{ x \mid P_1(x) \land P_2(x) \}
+</latex>
+<latex>
+(x \in S_1 \cap S_2) \leftrightarrow (x \in S_1 \land x \in S_2)
+</latex>
+===== Programs as relations =====
+Now back to meaning of programs.
+Simple programming language
+  x = exp
+  if (F) c1 else c2
+  c1 ; c2
+  while (F) c1
+Consider a program that manipulates two integer variables.
+What is the state - map from names to values.
+What is the meaning of
+  * x=y+3
+  * x=x+y
+  * x=y+3 ; x=x+y
+===== Programs as formulas =====
+Can we represent relations symbolically?
+In general? In our examples?
+<latex>
+  r = \{s \mid F(s(x),s(y)) \}
+</latex>
+Accumulation of equalities.
+===== Guarded command language =====
+Our simple language:
+  x = exp
+  if (F) c1 else c2
+  c1 ; c2
+  while (F) c1
+Guarded command language:
+  assume(F)
+  c1 [] c2
+  c1 ; c2
+  assert(F)
+  havoc(x)
+  c1*
+Relational semantics of guarded commands.
+Transforming language into guarded commands:
+  * conditionals:
+  if (F) c1 else c2
+=>
+  (assume(F); c1)  []
+  (assume(~F); c2)
+  * loops:
+  while (F) c1
+=>
+  (assume(F); c1)*;
+  assume(~F)
+   * loops, if we have loop invariants
+  while [inv I] (F) c1
+=>
+  assert(I);
+  havoc x1,...,xn;
+  assume(I);
+  (assume(~F) []
+   assume(F);
+   c1;
+   assert I;
+   assume(false));
+Transformations such as these are used in Jahob, ESC/Java, Spec#.
+===== Weakest Preconditions =====
+Weakest precondition of a set of states is the
+<latex>
+wp(r,P) = \{ s_1 \mid \forall s_2. (s_1,s_2) \in r \rightarrow s_2 \in P \}
+</latex>
+What happens if r is deterministic (a function on states)?
+Set of states - formula with state variables for one state.
+Relation on states - formula with state variables for two states.
+Important property: conjunctivity.
+<latex>
+  wp(r, P_1 \cap P_2) =
+</latex>
+Weakest preconditions for guarded commands.
+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}}.