# Differences

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

— |
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}}. | ||