# 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 [2015/04/21 17:30] (current) 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 21: Line 21: ===== Syntax Summary ===== ===== Syntax Summary ===== - $\begin{array}{l} + \begin{equation*}\begin{array}{l} F ::= A \mid F \land F \mid F \lor F \mid \lnot F \mid \exists x.F \mid \forall x.F \\ F ::= A \mid F \land F \mid F \lor F \mid \lnot F \mid \exists x.F \mid \forall x.F \\ A ::= R(T,​\ldots,​T) \mid T=T \mid S \subseteq S \mid S=S \\ A ::= R(T,​\ldots,​T) \mid T=T \mid S \subseteq S \mid S=S \\ Line 27: Line 27: U ::= f \mid U((T,​\ldots,​T):​=T) \\ U ::= f \mid U((T,​\ldots,​T):​=T) \\ S ::= V_s \mid S \cup S \mid S \cap S \mid S \setminus S \mid \{T,​\ldots,​T\} ​ S ::= V_s \mid S \cup S \mid S \cap S \mid S \setminus S \mid \{T,​\ldots,​T\} ​ - \end{array}$ + \end{array}\end{equation*} ===== Elimination of Extensions ===== ===== Elimination of Extensions ===== 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?