A first and very simple one consists in tracking the sign of variables. Imagine that + represents that a variable is greater than or equal to zero. Our analysis would be able to infer that, inside the body of the for loop variable i is +. This happens because i is initialized to zero, and then it is incremented by one (that is, a positive value is added to +, resulting still in a + value).
Another kind of abstraction might track the numerical interval of the possible values of variables. With this abstraction, we would track that i is [0..0] after initialization, and then, while iterating the abstract semantics of the for loop we will obtain the following sequence of intervals: [0..1], [0..2], [0..3], … For this abstraction, we need an operator that enforces the convergence of the analysis. Intuitively, this operator, after few iterations of the abstract semantics on the for loop, could approximate the value of i with the interval [0..+inf], reaching a so-called fixpoint in the analysis.
Applications of abstract interpretation to industrial software