Re: Conflicts between C standard and 754-2008
> Date: Mon, 03 Jan 2011 23:15:45 -0600
> From: Ralph Baker Kearfott <rbk5287@xxxxxxxxxxxxx>
> To: stds-754 <stds-754@xxxxxxxxxxxxxxxxx>,
> stds-1788 <stds-1788@xxxxxxxxxxxxxxxxx>
> Subject: Re: Conflicts between C standard and 754-2008
>
> Ah, yes, the standard might say one thing, while the implementation
> says another. However, without getting into the details of
> any aspect of any particular implementation being non-conforming,
> I'm wondering if a standard might be written in such a way
> to make it easier to make an implementation conforming.
> (As I say, I'm musing about a general principle.)
>
> Baker
>
> On 01/03/2011 03:13 PM, Vincent Lefevre wrote:
> > . . .
Ah, we can but try, my friend.
We can but try.
Seriously, making all our statements in a
mathematical or logical manner goes a long
way. But not far enough.
The principle I wanted to use in 754 was
to make sure that each statement that had
the word 'shall' in it also had a test for
that statement.
Alas, it is not often possible to write such
tests. Especially for any statement of the
form "For all x, y shall be true." And most
of our statements take on that form.
In the beginning, I had hopes of writing
test programs that at least tried to find the
worst cases of each such statement. But even
that can be difficult.
My best current hope is that the wonderful
work of our french friends might lead to
automated proofs that an implementation
conforms.
Even so, we must be careful how we write
things.
I'm just not sure how.
But, we can but try...
Dan