Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]


Groups > comp.lang.c > #64665

Re: More physical source files

From James Kuyper <jameskuyper@verizon.net>
Newsgroups comp.lang.c
Subject Re: More physical source files
Date 2015-07-04 12:23 -0400
Organization Self
Message-ID <55980890.5000104@verizon.net> (permalink)
References (6 earlier) <56d054c6-5316-46eb-b7b4-686bd405149d@googlegroups.com> <lnmvzf21kt.fsf@kst-u.example.com> <de40dc32-3557-4219-8eb8-c40d5481694d@googlegroups.com> <8761628png.fsf@bsb.me.uk> <559572FC.3030308@verizon.net>

Show all headers | View raw


On Friday, July 3, 2015 at 11:54:33 AM UTC-4, David Kleinecke wrote:
> On Thursday, July 2, 2015 at 10:21:10 AM UTC-7, James Kuyper wrote:
...
> > No, it is not. What "pedantic" does is guarantee that gcc fully conforms
> > to the specified version of the C (or C++) standard. Without -pedantic,
> >  -ansi only enables all features of C89 - it doesn't enable the
> > mandatory diagnostics for some gnu features that C89 considered to be
> > syntax errors or constraint violations.
> > The -pedantic option doesn't guarantee that all programs accepted by gcc
> > are strictly conforming. For the reasons given above, like all
> > real-world compilers, there are many ways for a program to have
> > undefined behavior that gcc is incapable of detecting.
>
> I was wrong about "pedantic" -  but it was only a guess.

The problem is not so much "-pedantic", but about what you thought it
meant. Your guess about what it meant was something it couldn't possibly
mean, for reasons that have nothing to do with the name of the option.

> As I have comment elsewhere I see a problem in what "unspecified"
> means. But surely you are right about undecidability under one
> interpretation of "unspecified".

Actually, the meaning of "unspecified" is irrelevant to my argument -
the key issue is "undefined behavior". Furthermore, it's not the meaning
of "undefined behavior" that is relevant, but the specific kinds of
things that the C standard says make the behavior of a program
undefined. The key feature is that, in some cases, the behavior is
undefined if two different pieces of code are both executed, even if
those pieces of code are widely separated both in time and in their
physical location in the code. There may be cases where the behavior is
merely "unspecified" when two widely separated pieces of code are
executed, and if that were the case, it would be sufficient in itself to
make it impossible to determine whether a piece of code is strictly
conforming. However, examples where the behavior is undefined come to my
mind much more readily.

> Assuming you conclusion, doesn't it follow that there is no test
> program that will tell us whether a given program is strictly
> conforming. ...

Of course. Such a test program would necessarily be able to solve the
halting problem, which has been proven to be impossible. If such a test
program could exist, it could be incorporated into a "strictly
compiling" implementation, to allow it to also be fully conforming.

> ... And therefore no algorithm for determining whether a
> compiler is conforming?

Of course there's no such algorithm. Treated as a black box, a compiler
is conforming only if it handles every possible program, when executed
with every possible input, in accordance with the requirements specified
by the standard. The only way to prove that a black box compiler is
conforming would be to pass it such a doubly-infinite set of test cases.
Note also that strictly conforming programs can contain infinite loops,
so infinitely many of the test cases will each take infinitely long to
complete. Failing any one of these test cases renders the implementation
non-conforming, no matter how many other test cases it passes.
Incorrectly translating a program that contains an infinite loop renders
the implementation non-conforming, even if the loop must keep running
for a billion years before the incorrect translation produces observable
effects.

If you don't treat an implementation as a black box, but actually
examine the details of how it is designed, I can't come up with an
argument that renders it impossible to determine that it's fully
conforming. However, it is extraordinarily difficult to prove that even
relatively simple programs are correct; and an implementation of C is
likely to be anything but simple. The C standard is 683 pages long, and
full conformance requires conforming to every requirement imposed by
every sentence in the normative parts of that document. And those
sentences are in English, not in some more formal specification
language. I don't think it's even possible to prove that the standard is
entirely self-consistent (it probably isn't - if I thought about it long
enough, I could probably even give you a known example). If it isn't
self-consistent, fully conforming with it would be impossible, so
proving that an implementation is fully conforming would also be impossible.

Whether code is "strictly conforming", and whether an implementation is
"fully conforming" are things that, in the general case, can only be
disproven by a finite example, they can't be proven. This is not
particularly unusual; it's a trait shared by most useful statements
about reality (for a particular definition of "useful").

Back to comp.lang.c | Previous | NextPrevious in thread | Next in thread | Find similar | Unroll thread


Thread

More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-06-27 11:19 -0700
  Re: More physical source files Malcolm McLean <malcolm.mclean5@btinternet.com> - 2015-06-27 11:54 -0700
    Re: More physical source files Ben Bacarisse <ben.usenet@bsb.me.uk> - 2015-06-27 21:20 +0100
  Re: More physical source files Bartc <bc@freeuk.com> - 2015-06-27 20:24 +0100
    Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-06-29 07:14 -0700
      Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-06-29 08:16 -0700
        Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-06-30 08:24 -0700
          Re: More physical source files Robert Wessel <robertwessel2@yahoo.com> - 2015-06-30 12:15 -0500
          Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-06-30 15:14 -0700
            Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-01 08:38 -0700
              Re: More physical source files glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2015-07-01 16:43 +0000
                Re: More physical source files Ben Bacarisse <ben.usenet@bsb.me.uk> - 2015-07-01 18:52 +0100
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-01 11:21 -0700
                Re: More physical source files glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2015-07-01 18:36 +0000
                Re: More physical source files Richard Damon <Richard@Damon-Family.org> - 2015-07-01 22:33 -0400
                Re: More physical source files glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2015-07-02 19:11 +0000
              Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-01 11:08 -0700
                Re: More physical source files Richard Damon <Richard@Damon-Family.org> - 2015-07-01 22:30 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-02 08:29 -0700
                Re: More physical source files Ben Bacarisse <ben.usenet@bsb.me.uk> - 2015-07-02 17:56 +0100
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-02 13:21 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-03 08:54 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-04 12:23 -0400
                Re: More physical source files Martin Shobe <martin.shobe@yahoo.com> - 2015-07-04 11:36 -0500
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-02 16:42 -0700
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-03 08:54 -0700
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-03 10:05 -0700
                Re: More physical source files glen herrmannsfeldt <gah@ugcs.caltech.edu> - 2015-07-03 21:57 +0000
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-04 00:30 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-04 08:08 -0700
                Re: More physical source files Richard Damon <Richard@Damon-Family.org> - 2015-07-04 12:21 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-05 09:22 -0700
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-05 09:49 -0700
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-05 18:16 -0700
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-06 08:37 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-06 12:56 -0400
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-06 11:59 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-06 15:45 -0400
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-06 13:14 -0700
                Re: More physical source files Philip Lantz <prl@canterey.us> - 2015-07-07 01:10 -0700
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-07 08:00 -0700
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-07 07:55 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-07 13:13 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-08 08:35 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-08 12:31 -0400
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-09 08:50 -0700
                Re: More physical source files Richard Heathfield <rjh@cpax.org.uk> - 2015-07-09 16:56 +0100
                Re: More physical source files Malcolm McLean <malcolm.mclean5@btinternet.com> - 2015-07-09 13:31 -0700
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-09 15:03 -0700
                Re: More physical source files Ian Collins <ian-news@hotmail.com> - 2015-07-10 10:54 +1200
                Re: More physical source files David Kleinecke <dkleinecke@gmail.com> - 2015-07-10 09:52 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-09 14:32 -0400
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-05 13:41 -0400
                Re: More physical source files Richard Damon <Richard@Damon-Family.org> - 2015-07-05 14:17 -0400
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-04 12:36 -0700
                Re: More physical source files Malcolm McLean <malcolm.mclean5@btinternet.com> - 2015-07-04 15:19 -0700
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-04 15:42 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-04 19:04 -0400
                Re: More physical source files Malcolm McLean <malcolm.mclean5@btinternet.com> - 2015-07-05 03:25 -0700
                Re: More physical source files Keith Thompson <kst-u@mib.org> - 2015-07-05 09:18 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-05 14:11 -0400
                Re: More physical source files Malcolm McLean <malcolm.mclean5@btinternet.com> - 2015-07-05 13:41 -0700
                Re: More physical source files Tim Rentsch <txr@alumni.caltech.edu> - 2015-07-10 19:00 -0700
                Re: More physical source files Tim Rentsch <txr@alumni.caltech.edu> - 2015-07-10 18:57 -0700
                Re: More physical source files James Kuyper <jameskuyper@verizon.net> - 2015-07-04 12:50 -0400
                Re: More physical source files Tim Rentsch <txr@alumni.caltech.edu> - 2015-07-11 08:39 -0700
      Re: More physical source files Bartc <bc@freeuk.com> - 2015-06-29 17:20 +0100
  Re: More physical source files Rosario19 <Ros@invalid.invalid> - 2015-06-28 11:57 +0200

csiph-web