This is an old revision of the document!
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 (quickly) the sign of \[
(31283321 + 8629184) \times (-34234) \times (-4 + (123123 \times (-3)))
\] Why?
What is (quickly) the sign of \[
(28166461706 + (723497 \times (- 38931))) \times 42
\]
Concrete domain:
Concrete operations:
Abstract domain:
Abstract operations: defined by tables:
Sign Analysis of Programs
Prove that this program never reports error:
i = 20; x = 2; while (i > 0) { x = x + 4; i = i - 1; } if (x==0) { error; } else { y = 1000/x; }
Abstract state: map each variable to element of . Here we have
possible states.
- computation over control-flow graph
What does it mean for such computation to be correct?