Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next 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> | ||
Line 326: | Line 327: | ||
\] | \] | ||
This is the semantics of the above code. | This is the semantics of the above code. | ||
+ | |||
Line 361: | Line 363: | ||
reduces to: | reduces to: | ||
\[ | \[ | ||
- | \forall v, v'. v' = v + 1 \rightarrow ( v > 0 \rightarrow v' > 0) | + | \forall v. \forall v'.\ v' = v + 1 \rightarrow ( v > 0 \rightarrow v' > 0) |
\] | \] | ||