Differences

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

--- sav08:sign_analysis_of_expressions_and_programs [2008/05/06 23:48]
vkuncak created
+++ sav08:sign_analysis_of_expressions_and_programs [2008/05/07 01:08]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Sign Analysis of Expressions and Programs ======
+===== Sign Analysis of Expressions =====
 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) * (-34234) * (-4 + 123123 * (-3))
+  (31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))
 \]
 Why?
+++++|
 \[
-   (pos \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 = \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 = \{ neg, nul, pos, \top \}$
+Abstract operations: $\oplus, \otimes : A^2 \to A$ defined by tables:
+===== Sign Analysis of Programs =====
+Prove that this program never reports error:
+<code>
+i = 20;
+x = 2;
+while (i > 0) {
+  x = x + 4;
+  i = i - 1;
+}
+if (x==0) {
+  error;
+} else {
+  y = 1000/x;
+}
+</code>
+Abstract state: map each variable to element of $A$.
+  * computation over control-flow graph
+What does it mean for such computation to be correct?