Differences
This shows you the differences between two versions of the page.
sav08:definition_of_set_constraints [2008/05/22 11:51] vkuncak |
sav08:definition_of_set_constraints [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ===== Definition of Set Constraints ===== | ||
- | |||
- | Set constraints are a logic used in program analysis. In set constraints, each variable denotes a set of ground terms. | ||
- | |||
- | Let $L$ be a language of function symbols and constants. We write $f \in L$ for an element of $L$. Let $GT$ be the set of ground terms in language $L$. | ||
- | |||
- | ==== Syntax of Set Constraints ==== | ||
- | |||
- | \[ | ||
- | \begin{array}{l} | ||
- | S ::= v | S \cap S | S \cup S | S \setminus S | f(S, ..., S) | f^{-i}(S) \\ | ||
- | F ::= S \subseteq S \mid F \land F | ||
- | \end{array} | ||
- | \] | ||
- | where | ||
- | * $v$ - set variable | ||
- | * $\cap,\cup,\setminus,\subseteq$ - standard set operations and relations | ||
- | * $f \in L$ - function symbol | ||
- | * in $f^{-i}$, $i$ is an integer between 1 and arity of $f$ | ||
- | |||
- | ==== Semantic ==== | ||
- | |||
- | * $v$ - set variable, subset of $GT$ | ||
- | * $\cap,\cup,\setminus,\subseteq$ - standard set operations and relations | ||
- | * $f(S_1,\ldots,S_n) = \{ f(t_1,\ldots,t_n) \mid t_1 \in S_1,\ldots, t_n \in S_n \}$ | ||
- | * $f^{-i}(S) = \{ t_i \mid f(t_1,\ldots,t_n) \in S \}$ | ||
- | |||
- | === Example1 === | ||
- | |||
- | \[ | ||
- | f(\{a,f(b,b)\},\{b,c\}) = \{ f(a,b),f(a,c),f(f(b,b),b), f(f(b,b),c) \} | ||
- | \] | ||
- | |||
- | === Example2 === | ||
- | |||
- | \[ | ||
- | f^{-2}(\{a,f(a,b),f(f(a,a),f(c,c))\}) = \{b,f(c,c)\} | ||
- | \] | ||
- | |||
- | === Example3 === | ||
- | |||
- | What is the least solution of constraints | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | a \subseteq S \\ | ||
- | f(f(S)) \subseteq S | ||
- | \end{array} | ||
- | \] | ||
- | where $a$ is constant and $f$ is unary function symbol. | ||
- | |||
- | === Example4 === | ||
- | |||
- | What is the least solution of constraints | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | a \subseteq S \\ | ||
- | black(S) \subseteq S \\ | ||
- | red(black(S)) \subseteq S | ||
- | \end{array} | ||
- | \] | ||
- | where $a$ is constant, $red,back$ are unary function symbols. | ||
- | |||
- | === Example5 === | ||
- | |||
- | Let $L = \{a_1,\ldots,a_n, not, and, or, implies\}$ where | ||
- | * $a_1,\ldots,a_n$ are constants representing propositional constants | ||
- | * $not$ is unary function symbol representing negation in abstract syntax tree | ||
- | * $and,or,implies$ are binary function symbols representing $\land,\lor,\rightarrow$ in syntax tree | ||
- | |||
- | Then the set of ground terms $GT$ represents propositional formulas. | ||
- | |||
- | What does the least solution of these constraints represent (where $S$,$P$ are set variables): | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | a_1 \subseteq P \\ | ||
- | \ldots \\ | ||
- | a_n \subseteq P \\ | ||
- | P \subseteq S \\ | ||
- | not(P) \subseteq S \\ | ||
- | and(S,S) \subseteq S \\ | ||
- | or(S,S) \subseteq S | ||
- | \end{array} | ||
- | \] | ||
- | |||
- | |||
- | ===== Existence of Solutions ===== | ||
- | |||
- | We were able to talk about "the least solution" because previous examples can be rewritten into form | ||
- | \[ | ||
- | (S_1,\ldots,S_n) = F(S_1,\ldots,S_n) | ||
- | \] | ||
- | where $F (2^{S})^n \to (2^{S})^n$ is a $\sqcup$-morphism (and therefore monotonic and $\omega$-continuous). The least solution can therefore be computed by fixpoint iteration (but it may contain infinite sets). | ||
- | |||
- | === Example === | ||
- | |||
- | Previous example can be rewritten as | ||
- | \[ | ||
- | \begin{array}{l} | ||
- | P = P \cup a_1 \cup \ldots a_n \\ | ||
- | S = S \cup P \cup not(P) \cup and(S,S) \cup or(S,S) | ||
- | \end{array} | ||
- | \] | ||
- | |||
- | Is every set expression in set constraints monotonic? ++|Set difference is not monotonic in second argument.++ | ||
- | |||
- | |||
- | ===== Conditional Constraints ===== | ||
- | |||
- | Let us simplify this expression: | ||
- | \[ | ||
- | f^{-2}(f(S,T)) = | ||
- | \] | ||
- | ++| | ||
- | \[ | ||
- | = f^{-2}(\{ f(s,t) \mid s \in S, t \in T \}) | ||
- | \] | ||
- | ++ | ||
- | ++| | ||
- | \[ | ||
- | = \{ s_1 \in S \mid \exists t_1 \in T \} | ||
- | \] | ||
- | ++ | ||
- | ++| | ||
- | \[ | ||
- | = \left\{ \begin{array}{rl} | ||
- | S, \mbox{ if } T \neq \emptyset \\ | ||
- | \emptyset, \mbox{ if } T = \emptyset | ||
- | \end{array} | ||
- | \right. | ||
- | \] | ||
- | ++ | ||