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_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. | ||