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_homework_2 [2007/03/28 14:38]
vkuncak 		sav07_homework_2 [2007/03/29 22:19]
vkuncak
Line 1: Line 1:
 ====== Homework 2 ====== ====== Homework 2 ======
 +
 +
 +
  
 ==== Quantifier Elimination ==== ==== Quantifier Elimination ====
  
-Consider a fragment of Presburger arithmetic where atomic formulas are equalities $v = u$ or inequalities of the form $v + c \leq u$, for arbitrary integer variables $u, v$ and arbitrary constants $c$.  Verify whether this language admits quantifier elimination. ​+Consider a fragment of Presburger arithmetic where atomic formulas are equalities $v = u$ or inequalities of the form $v + c \leq u$, for arbitrary integer variables $u, v$ and arbitrary constants $c$. 
 + 
 +  F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F 
 +  A ::= v=v | v + K <= v 
 +  K ::= ... -2 | -1 | 0 | 1 | 2 | ... 
 +  v ::= x | y | z | ...   
 + 
 +Verify whether this language admits quantifier elimination. ​
   * If it does admit quantifier-elimination,​ prove that this is the case by describing this algorithm informally, but precisely. ​ The algorithm should take a formula of the form Qx.F where Q is a quantifier and F is quantifier-free,​ and it should eliminate the quantifier. ​   ​   * If it does admit quantifier-elimination,​ prove that this is the case by describing this algorithm informally, but precisely. ​ The algorithm should take a formula of the form Qx.F where Q is a quantifier and F is quantifier-free,​ and it should eliminate the quantifier. ​   ​
   * If it does not admit quantifier elimination,​ give an example formula that you believe does not have a corresponding equivalent quantifier-free formula and describe constructs that you need to add to make quantifier elimination possible.   * If it does not admit quantifier elimination,​ give an example formula that you believe does not have a corresponding equivalent quantifier-free formula and describe constructs that you need to add to make quantifier elimination possible.
Line 13: Line 23:
 For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections. For in depth understanding you can also read references in there, in particular the relevant Wilfrid Hodges model theory book sections.
  
- +**Hint**: You should be able to reduce the problem to reasoning about conjunctions and generate a disjunction over total orders over terms of form v+c.  Alternatively,​ you may be able to use some ideas of [[http://​citeseer.ist.psu.edu/​71579.html|Fourier-Motzkin elimination]].
  
 ==== Verification condition generator ==== ==== Verification condition generator ====
Line 25: Line 34:
       | havoc(v,​...,​v)       | havoc(v,​...,​v)
       | S ; S       | S ; S
-      | while (F) { S } +      | while [inv F] (F) { S } 
       | if (F) { S } else { S }       | if (F) { S } else { S }
   T ::= T+T | T-T | K*T | v   T ::= T+T | T-T | K*T | v
Line 41: Line 50:
  
 This notation corresponds to a fragment of the language of the [[wk>​Isabelle theorem prover]], as well as the [[Jahob system]]. This notation corresponds to a fragment of the language of the [[wk>​Isabelle theorem prover]], as well as the [[Jahob system]].
 +
 +The notation for while loop indicates that all loops have supplied loop invariants.
  
 You do not need to build a parser for programs and formulas for this exercise, but it may make the testing of your implementation easier. You do not need to build a parser for programs and formulas for this exercise, but it may make the testing of your implementation easier.
  
-2. Given a statement S, compute wp(S,true) and pretty print it as a string conforming to the above grammar. ​ Test your program on +To make sure that you correctly avoid accidental variable capture, one of the many tests for your program should be the following 4 line sequence of commands: 
 + 
 +  x = 0; 
 +  y = x + 3; 
 +  havoc(x); 
 +  assert (y=3); 
 + 
 +2. Given a statement S, compute wp(S,​true) ​using the part 1, and pretty print it as a string conforming to the above grammar. ​ Test your program on 
   * two input programs that generate valid formulas   * two input programs that generate valid formulas
   * two input programs that generate invalid formulas   * two input programs that generate invalid formulas
 Try using the [[wk>​Isabelle theorem prover]] or formDecider in the [[Jahob system]] to prove the validity of the printed formulas and describe your experience. Try using the [[wk>​Isabelle theorem prover]] or formDecider in the [[Jahob system]] to prove the validity of the printed formulas and describe your experience.