Differences

This shows you the differences between two versions of the page.

--- sav08:sign_analysis_of_expressions_and_programs [2008/05/06 23:49]
vkuncak
+++ sav08:sign_analysis_of_expressions_and_programs [2008/05/07 00:09]
vkuncak
@@ Line 3: / Line 3: @@
 Suppose we want to test quickly whether the result of an expression is positive, negative or zero.
-What is the sign of
+What is (quickly) the sign of
 \[
   (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))
@@ Line 10: / Line 10: @@
 ++++|
 \[
-   (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg))
+   (pos \oplus pos) \otimes neg \otimes (neg \oplus (pos \otimes neg)) = pos \otimes neg \otimes neg = pos
 \]
 ++++
+What is (quickly) the sign of
+\[
+    (28166461706 + (723497 \times (- 38931))) \times 42
+\]
+++++|
+\[
+   (pos \oplus (pos \otimes neg)) \otimes pos = (pos \oplus neg) \otimes pos = \bot \otimes pos = \bot
+\]
+++++
+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, \bot \}$
+Abstract operations: $\oplus, \otimes : A^2 \to A$