This is an old revision of the document!
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 be a language of function symbols and constants. We write
for an element of
. Let
be the set of ground terms in language
.
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
- set variable
- standard set operations and relations
- function symbol
- in
,
is an integer between 1 and arity of
Semantic
- set variable, subset of
- standard set operations and relations
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 is constant and
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 is constant,
are unary function symbols.
Example5
Let where
are constants representing propositional constants
is unary function symbol representing negation in abstract syntax tree
are binary function symbols representing
in syntax tree
Then the set of ground terms represents propositional formulas.
What does the least solution of these constraints represent (where ,
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 is a
-morphism (and therefore monotonic and
-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} \]
Conditional Constraints
An important property we would like to have in this semantic is a very intuitive one : \[ f^{-1}(f(S_1, S_2)) = S_1 \] This property is in fact not conserved as we can easily see using a very simple counter-example : \[ f^{-1}(f(S_1, \emptyset)) = t_1 \in [[S_1 \wedge t_2 \in \emptyset \rbrace)]] = f^{-1}(\emptyset) = \emptyset \]
The correct interpretation of this property is :