gwyn@smoke.BRL.MIL (Doug Gwyn) (11/09/89)
In article <1989Nov8.225008.793@algor2.algorists.com> jeffrey@algor2.ALGORISTS.COM (Jeffrey Kegler) writes: >... A brave new world, where any question about dpANS could be stated >as a theorem and proved or disproved ... would seem a vast improvement. An additional drawback that you failed to mention in your article is that C is deliberately "fuzzy" in many areas, to permit efficient implementation on a variety of architectures. This makes it rather unsuitable to theorem proving, since useful theorems would have to be about C's behavior on entire classes of architectures.
jeffrey@algor2.algorists.com (Jeffrey Kegler) (11/09/89)
DG> Article <11571@smoke.BRL.MIL> gwyn@brl.arpa (Doug Gwyn)
JK> Article <1989Nov8.225008.793@algor2.algorists.com>
jeffrey@algor2.ALGORISTS.COM (Jeffrey Kegler)
JK> ... A brave new world, where any question about dpANS could be stated
JK> as a theorem and proved or disproved ... would seem a vast improvement.
DG> An additional drawback that you failed to mention in your article is
DG> that C is deliberately "fuzzy" in many areas, to permit efficient
DG> implementation on a variety of architectures. This makes it rather
DG> unsuitable to theorem proving, since useful theorems would have to be
DG> about C's behavior on entire classes of architectures.
I failed to mention it because I think denotational semantics deals
much better with "fuzziness" (if I understand what you mean by fuzzy)
than English. I assume you mean the same as Scott Daniels
(daniels@cse.ogc.edu) who (in Email to me) give the order of
evaluation of function arguments as an example of such.
[ Aside: there is such a thing as fuzzy logic, which I assume Doug
knows about, and I assume that is not what he means, hence his use of
quote marks. ]
By "fuzz", I believe we mean indeterminacy. [ Note that
implementation specific behavior is included in this concept of
indeterminacy. ] Even though the physical machine on which C runs will
probably be determinate (dpANS does not require it to be), the virtual
machine dpANS describes is not determinate. Of course, all sorts of
results can be proved about indeterminate machines.
[ Definitions: "determinacy" means that give one state of an abstract
machine, we can uniquely determine the succeeding one. Indeterminacy
means a given state of the virtual machine could result in any of one
or more succeeding states. ]
Take as an simple example of "fuzz":
r = rand();
r = r * r;
I cannot say what r is after these two statements, but I can prove
theorems about it nonetheless. The theorem "r is greater than zero,
or r has overflowed or a signal has been handled or the implementation
is not hosted" for example, can be shown to be true (if I remembered
all the appropriate conditions).
For example, the result of
int f(int a, int b) { return a+b; }
...
i = 2; i = f(i = 3, i);
is indeterminate. Variable i can be either 5 or 6, after this
(untested and unrecommended) code fragment.
--
Jeffrey Kegler, Independent UNIX Consultant, Algorists, Inc.
jeffrey@algor2.ALGORISTS.COM or uunet!algor2!jeffrey
1762 Wainwright DR, Reston VA 22090henry@utzoo.uucp (Henry Spencer) (11/10/89)
In article <1989Nov8.225008.793@algor2.algorists.com> jeffrey@algor2.ALGORISTS.COM (Jeffrey Kegler) writes: >... A brave new world, where >any question about dpANS could be stated as a theorem and proved or >disproved (or, much less likely, found undecidable), would seem a vast >improvement. Maybe. Remember that "proved" and "disproved" should really read "claimed to be [dis]proved" -- only God can consistently write error-free proofs. Certainly human mathematicians and program-verification people don't, as witness quite a few embarrassing errors in formally-refereed published papers purporting to be demonstrations of how to verify programs! A formal definition of C would inevitably be large and messy, especially given the many places where C refuses to promise how the machine behaves. I suspect that proving theorems from it would not be a simple exercise. -- A bit of tolerance is worth a | Henry Spencer at U of Toronto Zoology megabyte of flaming. | uunet!attcan!utzoo!henry henry@zoo.toronto.edu
perry@ccssrv.UUCP (Perry Hutchison) (11/10/89)
In article <1989Nov9.151708.3617@algor2.algorists.com> jeffrey@algor2.algorists.com (Jeffrey Kegler) writes: + the result of + + int f(int a, int b) { return a+b; } + ... + i = 2; i = f(i = 3, i); + + is indeterminate. Variable i can be either 5 or 6, after this It can also be 3. In fact, it is probably legal for i to have any value whatsoever, or for the program to dump core.
bill@twwells.com (T. William Wells) (11/11/89)
In article <1989Nov9.201125.8989@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes:
: Certainly human mathematicians and program-verification people don't, as
: witness quite a few embarrassing errors in formally-refereed published
: papers purporting to be demonstrations of how to verify programs!
:
: A formal definition of C would inevitably be large and messy, especially
: given the many places where C refuses to promise how the machine behaves.
: I suspect that proving theorems from it would not be a simple exercise.
Which leads us to: we finally would have a real use for all those
automatic theorem provers! 1/2 :-)
---
Bill { uunet | novavax | ankh | sunvice } !twwells!bill
bill@twwells.comgwyn@smoke.BRL.MIL (Doug Gwyn) (11/11/89)
In article <1989Nov9.151708.3617@algor2.algorists.com>, jeffrey@algor2.algorists.com (Jeffrey Kegler) writes: > I cannot say what r is after these two statements, but I can prove > theorems about it nonetheless. The theorem "r is greater than zero, > or r has overflowed or a signal has been handled or the implementation > is not hosted" for example, can be shown to be true (if I remembered > all the appropriate conditions). Oh, I agree that theorems like that could be proved, but what would be the point? You can already tell that much without a formal denotational semantics specification for C. Areas where formal semantics MIGHT be useful would include the effect of preprocessing, determining type compatibility, and applying conversion rules. I'm not sure it would be easier to work those out using formal symbolism instead of the technical English rules, however. And it would seem that one needs the natural-language formulation anyway in order to write programs.
gwyn@smoke.BRL.MIL (Doug Gwyn) (11/11/89)
In article <1989Nov9.201125.8989@utzoo.uucp> henry@utzoo.uucp (Henry Spencer) writes: >Maybe. Remember that "proved" and "disproved" should really read "claimed >to be [dis]proved" -- only God can consistently write error-free proofs. >Certainly human mathematicians and program-verification people don't, as >witness quite a few embarrassing errors in formally-refereed published >papers purporting to be demonstrations of how to verify programs! My favorite was an example in Dijkstra's classic "A Discipline of Programming" where he claimed that he hadn't submitted his program to operational testing since it had been created using a discipline that guaranteed it would be correct. Naturally, there were a couple of bugs in it!
jeffrey@algor2.algorists.com (Jeffrey Kegler) (11/11/89)
PH> Article <813@ccssrv.UUCP> perry@ccssrv.UUCP (Perry Hutchison)
JK> Article <1989Nov9.151708.3617@algor2.algorists.com>
jeffrey@algor2.algorists.com (Jeffrey Kegler)
JK> the result of
JK>
JK> int f(int a, int b) { return a+b; }
JK> ...
JK> i = 2; i = f(i = 3, i);
JK>
JK> is indeterminate. Variable i can be either 5 or 6, after this
PH> It can also be 3. In fact, it is probably legal for i to have any value
PH> whatsoever, or for the program to dump core.
I checked this before posting. Evaluation order of arguments is
covered by 3.3.2.2 which treats this as unspecified behavior, not
undefined behavior. (See also A.6.1). So no core dumps are allowed
in conforming implementations.
As for 3 being a possible result, the function call is a sequence
point (A.2 and 3.3.2.2), as is the expression in the return statement
(3.6). So the addition must be performed prior to the assignment
(2.1.2.3).
--
Jeffrey Kegler, Independent UNIX Consultant, Algorists, Inc.
jeffrey@algor2.ALGORISTS.COM or uunet!algor2!jeffrey
1762 Wainwright DR, Reston VA 22090rob@raksha.eng.ohio-state.edu (Rob Carriere) (11/14/89)
In article <11580@smoke.BRL.MIL> gwyn@smoke.BRL.MIL (Doug Gwyn) writes: >In article <1989Nov9.151708.3617@algor2.algorists.com>, jeffrey@algor2.algorists.com (Jeffrey Kegler) writes: >> I cannot say what r is after these two statements, but I can prove >> theorems about it nonetheless. The theorem "r is greater than zero, >> or r has overflowed or a signal has been handled or the implementation >> is not hosted" for example, can be shown to be true (if I remembered >> all the appropriate conditions). > >Oh, I agree that theorems like that could be proved, but what would be >the point? You can already tell that much without a formal denotational >semantics specification for C. Hmmm.... You would sure hope so, or there's a bad problem with the Standard. However, that seems to me a lot like the argument that we should all program in assembly, 'cause it is Turing-complete. The argument started with the assertion that it would be _easier_ to show those things in a formal semantic system. I am not sure whether that is true, especially for denotational semantics (I am still impressed by a calculation of the meaning of "if B then goto L;" which took a full page of densely written math!), but it seems to me whether or not one can with sufficient effort do something with the existing methods is beside the point. >Areas where formal semantics MIGHT be useful would include the effect of >preprocessing, determining type compatibility, and applying conversion >rules. I'm not sure it would be easier to work those out using formal >symbolism instead of the technical English rules, however. Possibly not. However, there are very few people who agree completely just what the rules of technical English are. Also, having to express the intent in a formalism where one cannot accidentely skip some details might make the process of writing a standard more accurate. I have at least personally found that having to mathematize (sorry :-) my ideas is one good way to discover what I don't quite understand yet. >And it would >seem that one needs the natural-language formulation anyway in order to >write programs. Very probably true. However, a compiler writer with training in formal semantics might well bless the standards commitee that comes out with a formal definition (maybe she'd even send them flowers :-) SR