LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav07_lecture_3 [2007/04/11 13:51]
vkuncak
sav07_lecture_3 [2007/04/18 09:39] (current)
kremena.diatchka
Line 56: Line 56:
  
   assume true  = skip   (does nothing)   assume true  = skip   (does nothing)
 +
  
 ==== Composing formulas using relation composition ==== ==== Composing formulas using relation composition ====
Line 67: Line 68:
 In sequential composition we follow the rule for composition of relations. ​ We want to get again formula with free variables x_0,​y_0,​x,​y. ​ So we need to do renaming. ​ Let x_1,​y_1,​error_1 be fresh variables. In sequential composition we follow the rule for composition of relations. ​ We want to get again formula with free variables x_0,​y_0,​x,​y. ​ So we need to do renaming. ​ Let x_1,​y_1,​error_1 be fresh variables.
  
-  CR(c1 ; c2) = exists x_1,​y_1,​error_1. ​ CR(c1)[x:​=x_1,​y:​=y_1,​error:​=error_1] & CR(c2)[x:=x_1,y:=y_1,error:=error_1]+  CR(c1 ; c2) = exists x_1,​y_1,​error_1. ​ CR(c1)[x:​=x_1,​y:​=y_1,​error:​=error_1] & CR(c2)[x_0:=x_1,y_0:=y_1,error_0:=error_1]
  
 The base case is The base case is