Differences
This shows you the differences between two versions of the page.
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 ==== |