LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_homework_4 [2007/04/24 22:22]
vkuncak 		sav07_homework_4 [2007/04/24 22:27] (current)
vkuncak
Line 141: Line 141:
  
 You can find some example formulas in jahob/​examples/​nasty_formulas directory of Jahob. You can find some example formulas in jahob/​examples/​nasty_formulas directory of Jahob.
 +
  
  
Line 221: Line 222:
  
 You can then pretty print such formulas and test their value using formDecider. You can then pretty print such formulas and test their value using formDecider.
 +
 +NOTE: To test your translation,​ you can use the fact that formDecider and Isabelle do, in fact, support '​if'​ expressions. ​ For example, if you give to formDecider the formula
 +
 +  ((if i=i+k then o2 else (if i=i then o1 else a(i))) = 
 +  (if i+k=i+k then o2 else (if i+k=i then o1 else a(i+k))))
 +
 +it will say that the formula is not valid, which is a correct answer. ​ On the other hand, if you give it the formula
 +
 +  (o1=o2 | k=0) --> ​
 +  ((if i=i+k then o2 else (if i=i then o1 else a(i))) = 
 +  (if i+k=i+k then o2 else (if i+k=i then o1 else a(i+k))))
 +
 +it will correctly conclude that the formula is valid.
  
 ==== Verifying programs with procedures ==== ==== Verifying programs with procedures ====