LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:fol_with_update_expressions [2008/04/09 00:17]
vkuncak
sav08:fol_with_update_expressions [2015/04/21 17:30] (current)
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 =====+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?