|
Prev: Teaching OO
Next: multimethod + multiple inheritance
From: Miguel Oliveira e Silva on 28 Feb 2006 18:47 "Daniel T." wrote: > In article <4404AB97.37B38F68(a)det.ua.pt>, > Miguel Oliveira e Silva <mos(a)det.ua.pt> wrote: > > > No it is not. It is only necessary a little effort to understand > > what I'm saying, and what DbC is. > > [B. Meyer, Object-Oriented Software Construction, 2ed, > > pages 331-438] > > I understand DbC, but DbC is not what I've been discussing here. Ok. But "Water Cooler v2"'s initial message was clearly referring to DbC. > Preconditions existed long before Mr. Meyer. > Maybe it would avoid confusion if you used 'require' instead. DbC is a very useful tool in any language (not just Eiffel). > As in, "a require clause will cause an exception if its condition is > false." This is very different from what happens if a precondition is > not met. What do you propose that should happen in such situations? In my opinion either: 1. The error is detected statically and program is simply not allowed to run (the ideal solution); 2. The errors cannot be detected statically, but there is the possibility to trace them at runtime through runnable assertions. Regardless of this dynamic typed alike approach, the program is incorrect and it should behave appropriately (terminate immediately or raise an exception to allow a fault tolerant alternative path); 3. The error cannot be detected neither statically nor within runnable assertions. In this case since I'm an atheist there are not much things I could do... Nevertheless, sooner or later (hopefully, sooner) a runnable assertion will most likely fail (although not where it should). Do you have alternative proposals? > pre?con?di?tion: n : A condition that must exist or be established > before something can occur or be considered; a prerequisite. Exactly. > If a precondition is not met, the behavior of the code cannot even be > considered... Agreed. The program is incorrect (the error is somewhere within the caller's code). However the less the program is allowed to normally proceed after the error detection, the better (the error localization is much more precise, and devising fault tolerant algorithms are much easier and safe). > With DbC we can wonder what would happen if I sent 0 to the inverse > function, because there is a defined result (an exception will be > generated.) In DbC that's an exceptional behavior (due to a programming error), not a normal behavior. > Here, I've been talking about real preconditions, ones that > require being met or we cannot determine the outcome. All preconditions (postconditions, invariants and other assertions) are required to be met in correct programs. So I think I've been talking about the same things. DbC prescribes a very simple and precise behavior. If you have alternative practical proposals -based on the mathematical foundations in which most likely we all agree- I'm all ears. -miguel -- Miguel Oliveira e Silva
From: Miguel Oliveira e Silva on 28 Feb 2006 19:40 "Dmitry A. Kazakov" wrote: > On Tue, 28 Feb 2006 19:59:19 +0000, Miguel Oliveira e Silva wrote: > > > "Dmitry A. Kazakov" wrote: > > > >> On Tue, 28 Feb 2006 16:38:41 +0000, Miguel Oliveira e Silva wrote: > >> > >>> Exceptions exist as a > >>> mean to deal with (detectable) incorrect programs > >>> (in DbC it is as simply as this). > >> > >> Exceptions are used for control flow in correct programs. > > > > Not in DbC. That would be an unacceptable abuse of exceptions. > > > > A correct program should never raise exceptions. > > ??? > > >> Exceptions in incorrect programs are presumably incorrect. > > > > Nope. They *correctly* signal an *incorrect* program > > (as in physical sciences when an experience whose results > > contradicts what was expected from a theoretical law, > > proves *correctly* that the law is *incorrect*). > > Whom they signal to? In the case of a false precondition, to the routine's client. > To the incorrect program? Exactly. > What could an *incorrect* > program *correctly* do about anything? Terminate execution (identifying the error); or propagate the exception upwards in the call stack until a point in which it would be safe to retry an alternative (hopefully, correct) algorithm (fault tolerance). > Why would you trust to what an > incorrect program says? It is precisely because we can't trust an incorrect program, that an exception should be raised (otherwise, there would be no reason for not allowing the program to proceed normally). > Program: "I am a liar." > > Is it? (To be or not to be, that's the question!) > >> Extended numeric sets are proven to be mathematically correct and deliver > >> far safer and efficient computations than ones defined on bound numeric > >> subsets. NaN is a *legal* value of IEEE float. > > > > (So what?) > > > > I fail to see suitable uses of a NaN number ("Not-a-Number" number) > > other than to express an error within the number representation, > > It is the same misunderstanding as above. NaN is not an error, it is not a > number. As I said before, in 99.9...9% of the uses of the inverse(0) function it will be the result of a programming error (regardless of NaN). > It is like i=sqrt(-1), which is also not a [real] number, but an > ideal from another set [of complex numbers.] It is not like complex numbers, because to my knowledge there is no practical use for NaN (other than error signaling, for which there is a much better programming tool: exceptions). In R, I agree with you that the problem is the same in both situations: a programming error (located in the caller). > > but - by all means - be free to use that defensive approach to > > inverse [inverse(0) = NaN]. > > IEEE floats don't form a ring. So the theorem above does not hold. So what? > > > Just don't forget that the inverse function (as all functions) are > > is not an end in it selves, but a mean to reach somewhere. > > I'll bet that in 99.99...99% if the times the client of inverse > > is not expecting to divide by zero, neither such result makes > > any sense to whatever calculation required the use of this > > function. > > That does not influence program correctness. A nice thing about ideals, > like NaN, is that they don't leak. If an algorithm is correct in R without > ideals it stays in R with ideals. So it is 100% safe. You can continue with > NaN to the point where R is needed. Note, not as a precondition, but as a > type conversion. This conversion will raise an exception for NaN. That > would be a correct behavior. So you agree with me that the appropriate (exceptional) behavior as a result to a use of NaN would be to raise an exception? (We are getting somewhere.) Of course in my opinion, the error source is not due to the use of NaN. It is due to the part of program that was responsible for its existence (but that just my opinion). > >>>> Now that's a *real* precondition. > >>> > >>> What do you mean by "real"? > >> > >> = used to determine correctness of the program. > > > > What? > > > > Are you saying that the non-zero x precondition > > of inverse is not useful to determine the correctness > > of a program? > > No. I claim that only one of the following two statements is true for a > given program: > > 1. A predicate is a "real" precondition <=> determines correctness => its > value is not used (handled) by the program > > 2. A predicate is not a precondition => its value can be handled. So you prescribe a defensive programming technique when your compile time tools are unable to prove the correctness of preconditions (and what about other assertions?), even when it would be trivial to use them at runtime as in DbC? (Fine, just don't call it DbC.) > >>> (Surely you are not stating that runnable > >>> preconditions are not real!) > >> > >> That is the only possibility, as I have shown in our previous discussion. > > > > (I missed that demonstration.) > > pre: true > function Liar return Boolean is > begin > return not Correct (Liar); > end Liar; > post : Liar > If things determining the program correctness were allowed for evaluation > in the program, that would allow construction of the liar paradox. That's the problem of searching for total correctness (or the "truth" in science) The much more practical and non-paradoxal search for incorrect programs is much easier (as it is to search for incorrect scientific theories). > So if a precondition determines correctness, A precondition (or any other assertion) states a correctness condition. It does not prove, by itself, the correctness of a program (it is a mean, not an end). > then it cannot be checked (=it > is "real"). If it is checked [and the system is not self-contradictory], > then it does not determine the correctness => it is not a precondition. Runnable assertions cannot fully assert program correctness (for the nth+2 times). They allow the detection of *incorrect* programs (if, and only if, the assertion happens to be false somewhere during program execution). A runnable precondition is a practical approximation of the formal mathematical precondition expected to be observed. It cannot prove program correctness. It can, nevertheless, detect program incorrectness (why is this so difficult to understand?). > > If that is your opinion, then don't call it DbC, or else you > > will be confusing everyone who does not know what is > > this methodology. > > So in your opinion the "real" DbC is self-contradictory? No. (A reference for your real "DbC" would be most welcomed, so that we may communicate with each other.) > Cool! > > -- > Regards, > Dmitry A. Kazakov > http://www.dmitry-kazakov.de Best regards, -miguel -- Miguel Oliveira e Silva
From: Martin Brown on 1 Mar 2006 04:14 Daniel T. wrote: > In article <du2530$jog$1(a)newsg4.svr.pol.co.uk>, > Martin Brown <|||newspam|||@nezumi.demon.co.uk> wrote: > >>Daniel T. wrote: >>>The precondition of course is that 'x != 0' however, thats an easy thing >>>to check, and as such one can define a particular output for that >>>condition: >>> >>>// returns NaN if x == 0 >>>double inverse( double x ) { >>> return 1/x; >>>} >> >>Although you could specify it to return a silent NaN that merely delays >>detecting a hard error and contaminates other possibly meaningful future >>calculations that use this NaN result. >> >>Generating a trap in most cases would be preferable since it usually >>signifies a serious programming error when division by zero occurs. > > I have no problem with that, it's still a defined result. More importantly it isolates the failing code and broken contract as soon as is reasonably possible. There isn't much point in continuing a calculation with a runtime lash up flying on a wing and a prayer. Anything that uses the Nan becomes contaminated wasting time and money. >>Your improved definition potentially breaks some code that might be >>expected to work algebraically since you can no longer satisfy the >>invariant property for the function inverse for all valid inputs. >> >>x == inverse( inverse(x) ) >> >>whereas 0 != inverse( inverse(0)) under your definition. >> >>And at present inverse(Nan) is also undefined. > > We'd have to define that as well I guess. "ensure inverse(NaN) == 0" Why guess or use Nan at all when the hardware provides signed infinites? It is a very bad idea. One perfectly reasonable use for signalling NaNs in testing is to ensure that loading floating point numbers from uninitiallised variables will generate an immediate error interrupt. If you must allow inverse(0) it should return a signed Infinity (and IEEE floating point defines them) and that is what most FP hardware does by default but it also requests a zero divide interrupt unless masked. Regards, Martin Brown
From: Dmitry A. Kazakov on 1 Mar 2006 06:22 On Wed, 01 Mar 2006 00:40:11 +0000, Miguel Oliveira e Silva wrote: > "Dmitry A. Kazakov" wrote: > >> Why would you trust to what an >> incorrect program says? > > It is precisely because we can't trust an > incorrect program, that an exception should > be raised (otherwise, there would be no reason > for not allowing the program to proceed > normally). But an exception is a way to convey something. How can you trust it? >> Program: "I am a liar." >> >> Is it? > > (To be or not to be, that's the question!) Don't trust in what a program tells, look what it does! >>>> Extended numeric sets are proven to be mathematically correct and deliver >>>> far safer and efficient computations than ones defined on bound numeric >>>> subsets. NaN is a *legal* value of IEEE float. >>> >>> (So what?) >>> >>> I fail to see suitable uses of a NaN number ("Not-a-Number" number) >>> other than to express an error within the number representation, >> >> It is the same misunderstanding as above. NaN is not an error, it is not a >> number. > > As I said before, in 99.9...9% of the uses of the inverse(0) function > it will be the result of a programming error (regardless of NaN). Where you get this statistics? In practically any correct numeric application you are unable to ensure that numeric underflows will not lead to a zero. Zero is a reachable state. So inverse(0) is quite legal, and the result NaN is also legal. It is not an error. Neither it indicates an error. If the algorithm is correct, NaN denotes a result outside the interval of finite values representable by double. That is a *correct* answer! You cannot depict any given value as damned. In the floating-point model each algorithm has some accuracy Eps (maybe dependant on the input.) It is a part of the contract. If the theoretically known result x deviates from the evaluated result y by less than Eps>0, then the algorithm is correct for the given input. So if x is the maximal finite double, then for any Eps NaN is a correct output. >> It is like i=sqrt(-1), which is also not a [real] number, but an >> ideal from another set [of complex numbers.] > > It is not like complex numbers, because to my knowledge > there is no practical use for NaN (other than error > signaling, for which there is a much better programming > tool: exceptions). No, exceptions were inappropriate here. If we consider closed operation 1/x defined on a numeric type. Then its definition depends on that type. Note that double (assuming IEEE float) and, say, DEC floating-point type, are different types with different sets of values! It is *incorrect* to raise an exception for double 1/x because 1/0 is *defined* to return NaN for 1/0. Defined here, is in strict mathematical sense. If you take another type, with the domain set limited to only real numbers (like DEC floating-point is), then exception would be appropriate. The above analysis considers closed 1/x, i.e. one, which result is of the same type as the argument. There could be cross variants. >> That does not influence program correctness. A nice thing about ideals, >> like NaN, is that they don't leak. If an algorithm is correct in R without >> ideals it stays in R with ideals. So it is 100% safe. You can continue with >> NaN to the point where R is needed. Note, not as a precondition, but as a >> type conversion. This conversion will raise an exception for NaN. That >> would be a correct behavior. > > So you agree with me that the appropriate (exceptional) behavior > as a result to a use of NaN would be to raise an exception? Not at all! You have to state the contract first. If "using" applies to the type double, then NaN is a legal value. If it is not of double type but of some other type, maybe, based on double, which does not contain NaN as a value, then you have to convert NaN to that type. (It is a typed world.) This would raise an exception. And again, not because of a contract violation. The contract states: double in, finite number or exception out. If you *excluded* exception from the postcondition, and let it propagate, then that would be a contract violation. >>>>>> Now that's a *real* precondition. >>>>> >>>>> What do you mean by "real"? >>>> >>>> = used to determine correctness of the program. >>> >>> What? >>> >>> Are you saying that the non-zero x precondition >>> of inverse is not useful to determine the correctness >>> of a program? >> >> No. I claim that only one of the following two statements is true for a >> given program: >> >> 1. A predicate is a "real" precondition <=> determines correctness => its >> value is not used (handled) by the program >> >> 2. A predicate is not a precondition => its value can be handled. > > So you prescribe a defensive programming technique when > your compile time tools are unable to prove the correctness > of preconditions (and what about other assertions?), No. You can prove correctness, you can do it at run-time, anything you want and have to, but *not* in the same program. A fault tolerant design assumes that there is a hierarchy of programs. Higher levels of the hierarchy can monitor lower levels. It is absolutely OK. Preconditions cannot be evaluated by the program, but they can be by another program. That program may run at the same computer (though better in a compiler.) When that program detects a contract violation, that would not raise an exception in a program under check. That would be wrong. It will abort the incorrect program. Technically it might look as an unhandled exception, but that is an implementation issue. The point is: whatever correctness checks are made they are outside. Another important point is, that the computing system as a whole, cannot check correctness of itself. The hierarchy must stop somewhere. >> pre: true >> function Liar return Boolean is >> begin >> return not Correct (Liar); >> end Liar; >> post : Liar > >> If things determining the program correctness were allowed for evaluation >> in the program, that would allow construction of the liar paradox. > > That's the problem of searching for total correctness > (or the "truth" in science) > > The much more practical and non-paradoxal search for incorrect > programs is much easier (as it is to search for incorrect scientific > theories). You can't gain anything practical from an incorrect theory. Note also that the correct theory gives you much more, than you think. It tells that run-time checks are the behavior [of the thing doing the checks.] This is a very valuable knowledge, which instructs developers to publish the checks in the contract. It also gives a rationale for layered fault-tolerant software design with layers insulated against faults underneath. Exactly because you cannot do much for correctness within one layer. This is IMO *true* Design by Contract! -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de
From: Dmitry A. Kazakov on 1 Mar 2006 08:46
On Tue, 28 Feb 2006 18:57:15 GMT, Daniel T. wrote: > We'd have to define that as well I guess. "ensure inverse(NaN) == 0" No. Consider: NaN = NaN * 0 Inverting both sides (we have an inverse now) and assuming that * and / are associative and distributive: 1/NaN = 1/NaN * 1/0 <=> 0 = 0 * NaN <=> 0 = NaN (oops!) Multiplicative inverse cannot be saved this way because NaN / NaN is not 1. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de |