Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_23 [2007/07/02 17:14] simon.blanchoud |
sav07_lecture_23 [2015/04/21 17:32] (current) |
||
---|---|---|---|
Line 67: | Line 67: | ||
We can then introduce $S_p$ as the set variable of the called methods : | We can then introduce $S_p$ as the set variable of the called methods : | ||
- | \[\forall p \in P . S_p \subseteq \left \lbrace m | \left ( info(p), m \right ) \in r^*, r = \lbrace (x,y) | x = over(y) \rbrace \right \rbrace \] | + | \begin{equation*}\forall p \in P . S_p \subseteq \left \lbrace m | \left ( info(p), m \right ) \in r^*, r = \lbrace (x,y) | x = over(y) \rbrace \right \rbrace \end{equation*} |
We also define $S_I$ as the set of all possibly called methods that we can build using the following formula : | We also define $S_I$ as the set of all possibly called methods that we can build using the following formula : | ||
- | \[ main \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \] | + | \begin{equation*} main \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \end{equation*} |
Line 111: | Line 111: | ||
Modularity: [[http://doi.acm.org/10.1145/316686.316703|Componential set-based analysis]] | Modularity: [[http://doi.acm.org/10.1145/316686.316703|Componential set-based analysis]] | ||
+ | |||
Line 123: | Line 124: | ||
* reduction to term algebras ({{http://theory.stanford.edu/~aiken/publications/papers/popl02.pdf|First-order theory of structural subtyping}}) | * reduction to term algebras ({{http://theory.stanford.edu/~aiken/publications/papers/popl02.pdf|First-order theory of structural subtyping}}) | ||
- | Deciding monadic class (({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) | + | ==== Term Algebras ==== |
- | * reduction to boolean algebras (MSOL fragment, has QE) | + | |
- | * small model property | + | * $L = \lbrace a, f, \ldots \rbrace$ |
- | * resolution variants | + | * $H$ : set of all ground terms |
+ | * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$ | ||
+ | This is First-Order Logic (FOL) with variables ! We can relate this to set constraints | ||
+ | |||
+ | |||
+ | |||
+ | ==== Monadic Class of FOL ==== | ||
+ | |||
+ | MFOL(({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) has : only unary predicates, no function symbol, quatifiers and logic. | ||
+ | |||
+ | Translating this to our sets language : | ||
+ | F := S = S | ||
+ | | S ⊆ S | ||
+ | | card(S) ≥ k | ||
+ | | card(S) = k | ||
+ | | F ∧ F | ||
+ | | ¬ F | ||
+ | | ∃v.F | ||
+ | S := v | ||
+ | | S ∪ S | ||
+ | | S ∩ S | ||
+ | | S' | ||
+ | | ∅ | ||
+ | | 1 | ||
+ | |||
+ | Where : | ||
+ | * $card(S) \geq k$ is syntactic sugar to represent a unary operator, as $k$ is not a variable, that compare the cardinality of $S$ with $k$ | ||
+ | * $k \geq 0$ is an integer | ||
+ | * $S'$ is the complement set of $S$ | ||
+ | * $1$ represents the whole universe | ||
+ | |||
+ | In order to agree with our definitions of set constraints, we need to eliminate : | ||
+ | * $S_1 = S_2 \rightarrow S_1 \subseteq S_2 \wedge S_2 \subseteq S_1 $ | ||
+ | * $S_1 \subseteq S_2 \rightarrow card(S_1 \cup S_2') = 0$ | ||
+ | |||
+ | We then have to be able to represent the following formulas : | ||
+ | * $\neg(card(s) \geq k) \rightarrow \bigvee_{i=0}^{k-1} card(S) = i$ | ||
+ | * $\neg(card(s) = k) \rightarrow card(S) \geq k+1 \vee \bigvee_{i=0}^{k-1} card(S) = i$ | ||
+ | |||
+ | We can then perform quantifier elimination. Note that this is not possible in case we do not have the $card$ operator : \begin{equation*}\exists v.card(S_1 \cap v) = k_1 \wedge card(S_1 \cap v') = k_2 \Rightarrow card(S_1) = k_1 + k_2\] | ||
+ | |||
+ | After elimination of the quantifiers, deciding the result of the formula is trivial. | ||