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/29 22:19] vkuncak |
sav07_homework_2 [2007/03/30 13:56] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Homework 2 ====== | ====== Homework 2 ====== | ||
| + | |||
| Line 23: | Line 24: | ||
| 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]]. | + | **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]], but it is not necessary for this problem to have an efficient algorithm, only an algorithm that works in principle. |
| + | |||
| ==== Verification condition generator ==== | ==== Verification condition generator ==== | ||
| Line 36: | Line 39: | ||
| | while [inv F] (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 | K |
| - | A ::= T=T | T < T | + | A ::= T=T | T < T | True | False |
| F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | F ::= A | (F&F) | (F|F) | ~F | ALL v.F | EX v.F | ||
| K ::= 0 | 1 | 2 | ... | K ::= 0 | 1 | 2 | ... | ||