# Differences

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

 sav08:fol_with_update_expressions [2008/04/09 00:17]vkuncak sav08:fol_with_update_expressions [2012/04/23 09:53]vkuncak Both sides previous revision Previous revision 2012/04/23 09:53 vkuncak 2008/04/09 00:23 vkuncak 2008/04/09 00:17 vkuncak 2008/04/09 00:16 vkuncak 2008/04/09 00:16 vkuncak 2008/04/09 00:15 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 20:55 vkuncak 2008/04/08 20:54 vkuncak 2008/04/08 17:26 vkuncak created Next revision Previous revision 2012/04/23 09:53 vkuncak 2008/04/09 00:23 vkuncak 2008/04/09 00:17 vkuncak 2008/04/09 00:16 vkuncak 2008/04/09 00:16 vkuncak 2008/04/09 00:15 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 23:55 vkuncak 2008/04/08 20:55 vkuncak 2008/04/08 20:54 vkuncak 2008/04/08 17:26 vkuncak created 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?