LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav07_homework_4 [2007/04/24 22:22]
vkuncak
sav07_homework_4 [2007/04/24 22:27]
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 202: 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 220: 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 ====