Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav07_lecture_2_skeleton [2007/03/17 20:06] (current)
vkuncak created
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}}.
  
 
sav07_lecture_2_skeleton.txt · Last modified: 2007/03/17 20:06 by vkuncak