Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:relational_semantics [2009/03/04 16:08] vkuncak |
sav08:relational_semantics [2009/03/04 17:55] vkuncak |
||
|---|---|---|---|
| Line 211: | Line 211: | ||
| * if it stops even if F is true, then assume(~F) at the end will give empty relation | * if it stops even if F is true, then assume(~F) at the end will give empty relation | ||
| Therefore, the result is equal to the correct number of execution times. | Therefore, the result is equal to the correct number of execution times. | ||
| + | |||
| ===== Summary of Simplifying the Language ===== | ===== Summary of Simplifying the Language ===== | ||
| Line 219: | Line 220: | ||
| c ::= x=T | assume(F) | c [] c | c ; c | loop c | c ::= x=T | assume(F) | c [] c | c ; c | loop c | ||
| - | Applying it to [[simple programming language|Collatz example]] we obtain | + | Applying it to a multiplication example, we obtain |
| <code> | <code> | ||