• English only

# Differences

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

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