Differences
This shows you the differences between two versions of the page.
sav08:fol_with_update_expressions [2012/04/23 09:53] vkuncak |
sav08:fol_with_update_expressions [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== FOL with Update Expressions ====== | ||
- | |||
- | Syntactic extension of FOL with if-then-else, function update, sets. | ||
- | |||
- | === If-Then-Else === | ||
- | |||
- | ite(p,x,y) = if p then x else y | ||
- | |||
- | === Function Update === | ||
- | |||
- | f (a:=b)(x) | ||
- | |||
- | f ( (a,b) :=c)(x,y) | ||
- | |||
- | === Sets === | ||
- | |||
- | Set variables (not quantified). | ||
- | |||
- | Set operations $\cup$, $\cap$, $\setminus$, $\{x,y\}$. | ||
- | |||
- | ===== Syntax Summary ===== | ||
- | |||
- | \[\begin{array}{l} | ||
- | 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 \\ | ||
- | T ::= V_o \mid U(T,\ldots,T) \mid ite(F,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\} | ||
- | \end{array}\] | ||
- | |||
- | ===== Elimination of Extensions ===== | ||
- | |||
- | 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))++ | ||
- | |||
- | z=ite(p,x,y) $\leftrightarrow$ ++| (p & z=x) | (~p & z=y) ++ | ||
- | |||
- | F(ite(p,x,y)) $\leftrightarrow$ ++|F(z) & z=ite(p,x,y)++ | ||
- | |||
- | S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++ | ||
- | |||
- | 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? | ||