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
sav07_homework_2 [2007/03/30 13:56]
vkuncak
sav07_homework_2 [2007/04/06 20:15]
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 ====
Line 32: Line 31:
 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)