Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:fol_with_update_expressions [2008/04/09 00:16] vkuncak |
sav08:fol_with_update_expressions [2008/04/09 00:23] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
=== Function Update === | === Function Update === | ||
- | f (a:=b)(x) = ++|ite(x=a,b,f(x))++ | + | f (a:=b)(x) |
- | f ( (a,b) :=c)(x,y) = ++|ite(x=a & y=b, c,f(x,y))++ | + | f ( (a,b) :=c)(x,y) |
=== Sets === | === Sets === | ||
Line 33: | Line 33: | ||
f(a:=b)(x) = ++|ite(x=a,b,f(x))++ | f(a:=b)(x) = ++|ite(x=a,b,f(x))++ | ||
- | f((a,b):=c)(x,y) = ++|ite(x=a & y=b, c,f(x,y))++ | + | f ( (a,b):=c )(x,y) = ++|ite(x=a & y=b, c,f(x,y))++ |
z=ite(p,x,y) $\leftrightarrow$ ++| (p & z=x) | (~p & z=y) ++ | z=ite(p,x,y) $\leftrightarrow$ ++| (p & z=x) | (~p & z=y) ++ | ||
Line 41: | Line 41: | ||
S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++ | S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++ | ||
- | ===== Substituting Function Symbols ===== | + | === Substituting Function Symbols === |
+ | Consider symbolic execution of assignment to local variable | ||
+ | x = e | ||
+ | Evaluate e in current symbolic state, then assign symbolic value of x to result. | ||
+ | |||
+ | Consider | ||
+ | x.f = e; | ||
+ | i.e. | ||
+ | f = f(x:=e) | ||
+ | We need to replace f with f(x:=e). | ||
+ | * do we always get syntactically valid formula in FOL extension above? | ||