LARA

Differences

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

Link to this comparison view

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:43]
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.
- 
- 
- 
- 
  
  
Line 69: Line 65:
  
 Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter. Benefit: if there is x_{n+1} that is not changed, we do not need to write its properties in the loop invariant. ​ This can make loop invariant shorter.
 +
 +==== References about weakest precondition (in construction) ====
 +  * Back, Wright: Refinement Calculus
 +  * Dijkstra
 +  * Hoare, He
  
 ===== Modeling data structures ===== ===== Modeling data structures =====
Line 81: Line 82:
  
 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 131:
  
 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 141:
 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 ==== +