Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:fol_with_update_expressions [2008/04/09 00:17] vkuncak |
sav08:fol_with_update_expressions [2012/04/23 09:53] vkuncak |
||
|---|---|---|---|
| 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 ===== | + | f = g ++| ALL x. f(x)=g(x) ++ |
| + | === 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? | ||