Re: Test tool not only for Ada

On Fri, 25 Jan 2008 08:48:35 -0000, Stuart wrote:

The interesting challenge for 'Abstract Interpretation' tools is deciding
how much detail to preserve at each stage. From the example should the tool
note that 'y' might have the values 2..40 or the set of values {2, 4, 6,
..., 40}.

This can become important, for instance if you had the statement:
z := 1000 / (y - 9);

Could a divide by zero occur? If you had a lax model of 'y' [2..40] you
would be concerned, but a more accurate model would dispel the concern.

There is another difficult aspect of the problem of uncertain computations.
It is dependency analysis. For example:

y := x;
z := x * y;

When x is in [-1, 2] then without knowing that y equals x, i.e. assuming
that x and y are independent, the best possible estimation of z is [-2, 4].
With this knowledge it is [0, 4].

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.