Lab for Automated Reasoning and Analysis 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
 
sav07_lecture_3.txt · Last modified: 2007/04/18 09:39 by kremena.diatchka
 
© EPFL 2018 - Legal notice