- English only

# Lab for Automated Reasoning and Analysis LARA

# Differences

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

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 ==== |