[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


754 | revision | FAQ | references | list archive