Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
sav07_homework_4 [2007/04/24 22:15] vkuncak |
sav07_homework_4 [2007/04/24 22:22] 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. | ||
| + | |||
| + | |||
| + | |||
| ==== Language features ==== | ==== Language features ==== | ||
| Line 189: | Line 192: | ||
| To do this, we eliminate array update expressions. A useful intermediate step is to represent array updates using conditional IF expressions. After replacing top-level updates the last expression becomes | To do this, we eliminate array update expressions. A useful intermediate step is to represent array updates using conditional IF expressions. After replacing top-level updates the last expression becomes | ||
| - | IF(i+k=i,o2,a[i:=o1](i)) = IF(i+k=i+k,o2,a[i:=o1](i+k)) | + | (if i+k=i then o2 else a[i:=o1](i)) = (if i+k=i+k then o2 else a[i:=o1](i+k)) |
| and then repeating the process we obtain | and then repeating the process we obtain | ||
| - | IF(i=i+k,o2,IF(i=i,o1,a(i))) = IF(i+k=i+k,o2,IF(i+k=i,o1,a(i+k))) | + | (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))) | ||
| - | We can in fact simplify some of these expressions and eliminate IF because we know the truth value, 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. |
| 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,o1,a(i)) & | + | (v1 = (if i=i then o1 else a(i))) & |
| - | v2 = IF(i=i+k,o2,v2) & | + | v2 = (if i=i+k then o2 else v2) & |
| - | v3 = IF(i+k=i,o1,a(i+k)) & | + | v3 = (if i+k=i then o1 else a(i+k)) & |
| - | v4 = IF(i+k=i+k,o2,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 208: | Line 212: | ||
| (v1=t1 & ... & vn=tn) --> F | (v1=t1 & ... & vn=tn) --> F | ||
| - | As a result, all IF expressions occur in formulas of form | + | As a result, all 'if' expressions occur in formulas of form |
| - | v = IF(c,t,e) | + | v = (if c then t else e) |
| which you can represent as | which you can represent as | ||