Re: Test tool not only for Ada

On Jan 25, 4:31 am, "Dmitry A. Kazakov" <mail...@xxxxxxxxxxxxxxxxx>
wrote:
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].

The SofCheck Inspector is another static analysis tool that
supports Ada. We keep track of the kinds of symbolic
relationships you mention (such as X = Y) in addition
to pure value range information.

Our website is http://www.sofcheck.com

You might check wikipedia for "static analysis" or
"source code analysis".


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

Sincerely,
-Tucker Taft
SofCheck, Inc.
Burlington, MA USA
.