• English only

# Differences

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

Link to this comparison view

sav07_homework_2 [2007/03/30 13:58]
vkuncak
sav07_homework_2 [2007/04/06 20:15] (current)
vkuncak
Line 1: Line 1:
====== Homework 2 ====== ====== Homework 2 ======
+

Line 10: Line 11:

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
-  A ::= v=v | v + K <= v+  A ::= v=v | v + K ≤ v
K ::= ... -2 | -1 | 0 | 1 | 2 | ...   K ::= ... -2 | -1 | 0 | 1 | 2 | ...
v ::= x | y | z | ...  ​   v ::= x | y | z | ...  ​
Line 25: Line 26:

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

==== Verification condition generator ==== ==== Verification condition generator ====

sav07_homework_2.txt · Last modified: 2007/04/06 20:15 by vkuncak

© EPFL 2018 - Legal notice 