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:16] vkuncak |
sav08:fol_with_update_expressions [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| 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 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 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 ===== | + | 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? | ||