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/05/26 12:54] 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 246: | Line 247: | ||
| \] | \] | ||
| In other words, assigning a variable is the same as changing it arbitrarily and then assuming that it has the right value. Under what condition does this equality hold? | In other words, assigning a variable is the same as changing it arbitrarily and then assuming that it has the right value. Under what condition does this equality hold? | ||
| + | |||
| + | |||
| + | ===== Summary of Correspondence between Programs and Relations ===== | ||
| + | |||
| + | # program construct # relational meaning # | ||
| + | | sequential composition | relation composition | | ||
| + | | branching | union | | ||
| + | | loops | transitive closure | | ||
| + | | assignment | update of one state component | | ||
| + | | havoc | arbitrary change of one state component | | ||
| ===== Control-Flow Graphs, While Theorem: One Loop is Enough ===== | ===== Control-Flow Graphs, While Theorem: One Loop is Enough ===== | ||
| Line 369: | Line 380: | ||
| * C A R Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998 | * C A R Hoare and He Jifeng. Unifying Theories of Programming. Prentice Hall, 1998 | ||
| * Semantics-based Program Analysis via Symbolic Composition of Transfer Relations, [[http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox/mosaic/papers/acid-thesis.ps|PhD dissertation by Christopher Colby]], 1996 | * Semantics-based Program Analysis via Symbolic Composition of Transfer Relations, [[http://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox/mosaic/papers/acid-thesis.ps|PhD dissertation by Christopher Colby]], 1996 | ||
| + | |||