• English only

# Differences

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

Link to this comparison view

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 