Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav07_homework_2 [2007/03/30 13:56] vkuncak |
sav07_homework_2 [2007/03/30 13:58] vkuncak |
||
|---|---|---|---|
| Line 25: | Line 25: | ||
| **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. | **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. | ||
| + | |||
| Line 32: | Line 33: | ||
| 1. Implement a verification condition generator that takes abstract syntax trees of the following form | 1. Implement a verification condition generator that takes abstract syntax trees of the following form | ||
| - | S ::= (x=T) | + | S ::= (v=T) |
| | assume(F) | | assume(F) | ||
| | assert(F) | | assert(F) | ||