Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_homework_4 [2007/04/24 22:21] 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 194: | Line 197: | ||
and then repeating the process we obtain | and then repeating the process we obtain | ||
- | (if i=i+k then o2 | + | (if i=i+k then o2 else (if i=i then o1 else a(i))) = |
- | 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))) |
- | (if i+k=i+k then o2 | + | |
- | else (if i+k=i then o1 else a(i+k))) | + | |
We can in fact simplify *some* of these 'if' expressions, but this is not necessary, and it is not possible in general. For example we cannot eliminate if i=i+k ... because we do now know the value of k. | We can in fact simplify *some* of these 'if' expressions, but this is not necessary, and it is not possible in general. For example we cannot eliminate if i=i+k ... because we do now know the value of k. | ||
Line 203: | Line 204: | ||
The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions. When proving validity of formulas, we can obtain, for example: | The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions. When proving validity of formulas, we can obtain, for example: | ||
- | (v1 = (if i=i then o1 else a(i))) & | + | (v1 = (if i=i then o1 else a(i))) & |
- | v2 = (if i=i+k then o2 else v2) & | + | v2 = (if i=i+k then o2 else v2) & |
- | v3 = (if i+k=i then o1 else a(i+k)) & | + | v3 = (if i+k=i then o1 else a(i+k)) & |
- | v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4 | + | v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4 |
You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables. If you have such a set of definitions of the form v1=t1, ..., vn=tn then if you are proving validity of formula F you use | You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables. If you have such a set of definitions of the form v1=t1, ..., vn=tn then if you are proving validity of formula F you use | ||
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 ==== |