From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Subject: Re: Test tool not only for Ada
Date: Fri, 25 Jan 2008 10:31:04 +0100
Date: 2008-01-25T10:31:05+01:00 [thread overview]
Message-ID: <3hudpxu5uku4.coi6mowz6oze$.dlg@40tude.net> (raw)
In-Reply-To: 47999e80$1_1@glkas0286.greenlnk.net
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
next prev parent reply other threads:[~2008-01-25 9:31 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2008-01-24 19:37 Test tool not only for Ada S�nke Brix
2008-01-24 21:20 ` Ludovic Brenta
2008-01-25 8:48 ` Stuart
2008-01-25 9:31 ` Dmitry A. Kazakov [this message]
2008-01-26 4:57 ` T. Taft
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox