Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
| 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> |
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 | Next — Previous in thread | Next in thread | Find similar | Unroll 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