Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
complexity [2007/10/04 23:15] philippe.suter |
complexity [2007/10/05 01:00] philippe.suter |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Complexity of the verification process ===== | ===== Complexity of the verification process ===== | ||
| + | |||
| ==== Preliminary remarks ==== | ==== Preliminary remarks ==== | ||
| Line 14: | Line 15: | ||
| === Consistency of the dimensions of the cartesian products === | === Consistency of the dimensions of the cartesian products === | ||
| - | We know that to every pattern corresponds one cartesian product. By construction, the dimension of these products is always the same since it corresponds to $max_p(E)$. In particular, this means that taking the union of two "pattern sets" will yield yet another cartesian product with the same cardinality. | + | For every pattern, we build a cartesian product representing the set of inputs which it would match. By construction, the dimension of these products is always the same since it corresponds to $max_p(E)$. In particular, this means that taking the union of two "pattern sets" will yield yet another cartesian product with the same cardinality. |
| Note that we now also have: | Note that we now also have: | ||
| Line 62: | Line 63: | ||
| \[ (S_1 \times \ldots \times S_n) \subseteq (A_1 \times \ldots \times A_n) \cup (\ldots) \cup (Z_1 \times \ldots \times Z_n) \] | \[ (S_1 \times \ldots \times S_n) \subseteq (A_1 \times \ldots \times A_n) \cup (\ldots) \cup (Z_1 \times \ldots \times Z_n) \] | ||
| - | When checking completeness, the set $(S_1 \times \ldots \times S_n)$ is the domain of the scrutinee, when checking reachability, it is the set of the observed pattern. (Note that this is in fact checking subsumption. Proper reachability checking would include verifying that the pattern set is a subset of the scrutinee set, but this does not introduce any additional complexity.) Also note that the sets over which the union is taken corresponds to patterns which satisfy one of these properties: | + | When checking completeness, the set $(S_1 \times \ldots \times S_n)$ is the domain of the scrutinee, when checking reachability, it is the set of the observed pattern. (Note that this is in fact checking subsumption. Proper reachability checking would include verifying that the pattern set is a subset of the scrutinee set, but this does not introduce any additional complexity.) Also note that the sets over which the union is taken correspond to patterns which satisfy one of the following properties: |
| * the pattern has no guard | * the pattern has no guard | ||
| * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement | * the pattern has a guard, but there exists a set of patterns with the same signature such that the disjunction of their guards is equivalent to the true statement | ||