From: Miguel Oliveira e Silva on
"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
"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
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
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
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
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
Prev: Teaching OO
Next: multimethod + multiple inheritance