Lab for Automated Reasoning and Analysis 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 ====
 
sav07_homework_4.txt · Last modified: 2007/04/24 22:27 by vkuncak
 
© EPFL 2018 - Legal notice