Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:relational_semantics [2009/03/04 17:55] vkuncak |
sav08:relational_semantics [2009/05/26 12:54] vkuncak |
||
---|---|---|---|
Line 247: | 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 370: | Line 381: | ||
* 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 | ||
+ |