Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_4_skeleton [2007/03/22 18:21] vkuncak |
sav07_lecture_4_skeleton [2007/03/22 20:34] vkuncak |
||
---|---|---|---|
Line 8: | Line 8: | ||
We use weakest preconditions, although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. | We use weakest preconditions, although you could also use strongest postconditions or any other variants of the conversion from programs to formulas. | ||
- | |||
- | |||
- | |||
- | |||
- | |||
===== More on wp ===== | ===== More on wp ===== | ||
Line 81: | Line 76: | ||
Array bounds checking. | Array bounds checking. | ||
+ | |||
==== Semantics of references ==== | ==== Semantics of references ==== | ||
Objects as references, null as an object. | Objects as references, null as an object. | ||
+ | |||
+ | 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> | ||
+ | |||
+ | left, right - uninterpreted functions (can have any value, depending on the program, unlike arithmetic functions such as +,-,* that have fixed interpretation). | ||
Null checks. | Null checks. | ||
Line 101: | Line 125: | ||
Again, the second part! More technical. But, often you can use these things as a black box. | Again, the second part! More technical. But, often you can use these things as a black box. | ||
+ | |||
==== Congruence closure algorithm ==== | ==== Congruence closure algorithm ==== | ||
Line 110: | Line 135: | ||
Equality is a congruence with respect to all function symbols. | Equality is a congruence with respect to all function symbols. | ||
- | + | More information on congruence closure algorithm: | |
- | ==== Basic idea of Nelson-Oppen combination ==== | + | * [[Gallier Logic Book]], Chapter 10.6 |
- | + | * {{nelsonoppen80decisionprocedurescongruenceclosure.pdf|the original paper by Nelson and Oppen}} | |
- | Consider quantifier-free formulas with both linear arithmetic and uninterpreted functions. | + | |
- | * disjunctive normal form | + | |
- | * flatten | + | |
- | * separate | + | |
- | * check satisfiability separately | + | |
- | + | ||
- | The harder part: proving that it is complete. | + | |
- | + | ||
- | Using a SAT solver to enumerate disjunctive normal form disjuncts. | + | |
- | + | ||
- | Standard for satisfiability checking of formulas, competition: http://combination.cs.uiowa.edu/smtlib | + | |
- | + | ||
- | Note: we can also encode entire formula into SAT. | + | |
- | + | ||
- | + | ||
- | ==== Quantified formulas ==== | + | |
- | + | ||
- | Notion of formal proof. | + | |
- | + | ||
- | Minimality and independence of axioms - not so important for us. | + | |
- | + | ||
- | Proof rules for first-order logic. | + | |
- | * propositional axioms | + | |
- | * instantiation | + | |
- | * generalization | + | |
- | + | ||
- | Example: axiomatizing some set operations. | + | |
- | + | ||
- | Two different techniques (recall we can take negation of formulas): | + | |
- | * Enumerating finite models (last time) gives us a way to show formula is satisfiable | + | |
- | * Enumerating proofs gives us a way to show that formula is valid | + | |
- | The gap in the middle: invalid formulas with only infinite models | + | |
- | * an example with only infinite models: strict partial order with no upper bound | + | |
- | + | ||
- | ==== Resolution theorem proving ==== | + | |
- | + | ||
- | From formulas to clauses | + | |
- | * negation normal form | + | |
- | * prenex form | + | |
- | * Skolemization | + | |
- | * conjunctive normal form | + | |
- | + | ||
- | Unification. | + | |
- | + | ||
- | Resolution and factoring proof rules. | + | |
- | + | ||
- | Theorem prover competition: http://www.cs.miami.edu/~tptp/ | + | |
- | + | ||
- | ==== Essentially propositional formulas ==== | + | |