Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:sign_analysis_of_expressions_and_programs [2008/05/07 00:09] 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 = \bot \otimes pos = \bot | + | (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \top \otimes pos = \top |
| \] | \] | ||
| ++++ | ++++ | ||
| Line 28: | Line 28: | ||
| Concrete operations: ${+}, {\times} : \mathbb{Z}^2 \to \mathbb{Z}$ | Concrete operations: ${+}, {\times} : \mathbb{Z}^2 \to \mathbb{Z}$ | ||
| - | Abstract domain: $A = \{ pos, neg, \bot \}$ | + | Abstract domain: $A = \{ pos, neg, \top \}$ |
| Abstract operations: $\oplus, \otimes : A^2 \to A$ | Abstract operations: $\oplus, \otimes : A^2 \to A$ | ||