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 | ||
sav08:sign_analysis_of_expressions_and_programs [2008/05/07 00:03] vkuncak |
sav08:sign_analysis_of_expressions_and_programs [2008/05/07 00:14] vkuncak |
||
---|---|---|---|
Line 20: | Line 20: | ||
++++| | ++++| | ||
\[ | \[ | ||
- | (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = ? \otimes pos = ? | + | (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top |
\] | \] | ||
++++ | ++++ | ||
+ | |||
+ | Concrete domain: $\mathbb{Z} = \{ \ldots, -2, -1, 0, 1, 2, \ldots \}$ | ||
+ | |||
+ | Concrete operations: ${+}, {\times} : \mathbb{Z}^2 \to \mathbb{Z}$ | ||
+ | |||
+ | Abstract domain: $A = \{ pos, neg, \top \}$ | ||
+ | |||
+ | Abstract operations: $\oplus, \otimes : A^2 \to A$ | ||
+ | |||