LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous 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 ​examplewe 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 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
 +