# 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

Why?

What is (quickly) the sign of

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?