LARA

Differences

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

Link to this comparison view

sav08:fol_with_update_expressions [2008/04/09 00:23]
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 ++ 
- 
-=== 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?