"require" and precondition

hello Eiffellers,

certainly i am nitpicking, but...
because of "require else", no "require" expression is definitely required.
it seems to me "require" suggests a necessary condition whereas the
precondition is actually a sufficient condition.
the point should be made clear in the final ETL3 book.
precondition being sufficient makes it clear enough that DbC is not merely
debugging.

- damien

>>>>> "damien" == damien guichardwanadoo fr <damien.guichardwanadoo.fr@wanad
oo.fr> writes:

damien> hello Eiffellers, certainly i am nitpicking, but...
damien> because of "require else", no "require" expression is
damien> definitely required.  it seems to me "require" suggests a
damien> necessary condition whereas the precondition is actually a
damien> sufficient condition.

Nope, it's a necessary precondition for that feature. That a redefined
feature might work in more cases is a separate issue.

--
Regards,

Berend.

** you're welcome to the #eiffel irc channel on irc.freenode.net

Berend de Boer wrote: 
>
>
>     damien> hello Eiffellers, certainly i am nitpicking, but...
>     damien> because of "require else", no "require" expression is
>     damien> definitely required.  it seems to me "require" suggests a
>     damien> necessary condition whereas the precondition is actually a
>     damien> sufficient condition.
>
> Nope, it's a necessary precondition for that feature. That a redefined
> feature might work in more cases is a separate issue.

A sufficient condition is one that is as strong as necessary or stronger.

If a designer specifies a precondition, he may make it stronger than he
requires, but that is a secret he holds to himself. All the client knows
is that the precondition is at least as strong as necessary.
--
Peter Horan                     School of Information Technology
peter@deakin.edu.au             Deakin University
+61-3-5227 1234 (Voice)         Geelong, Victoria 3217, AUSTRALIA
+61-3-5227 2028 (FAX)           http://www.cm.deakin.edu.au/~peter

-- The Eiffel guarantee: From specification to implementation
-- (http://www.cetus-links.org/oo_eiffel.html)

Peter Horan wrote:
> A sufficient condition is one that is as strong as necessary or stronger.
>
> If a designer specifies a precondition, he may make it stronger than he
> requires, but that is a secret he holds to himself. All the client knows
> is that the precondition is at least as strong as necessary.

I can understand your point. Perhaps a "or require" would have been better
than a "require else", making clear that the new precondition weakens the
old one instead of strengthening it.

For example:

require i > 10
or require i < 20
or require i.is_even

vs.

require i > 10
require else i < 20
require else i.is_even

On the other hand his issue just seems to confuse new Eiffel developers and
connected to the problem of understanding inheritance. Not that this is a
good thing (the language should be a clear as possible), but it should be
acceptable from a historical point of view. Also, precondition
redefinitions are very rare is real world problems.

Regards,
Bernd

>     damien> hello Eiffellers, certainly i am nitpicking, but...
>     damien> because of "require else", no "require" expression is
>     damien> definitely required.  it seems to me "require" suggests a
>     damien> necessary condition whereas the precondition is actually a
>     damien> sufficient condition.
>
> Nope, it's a necessary precondition for that feature. That a redefined
> feature might work in more cases is a separate issue.

It works the reverse way: because of "require", the "require else" condition
is not actually required, a "require else" condition is a sufficient
condition.
Nothing can be guaranteed by a necessary condition.
No necessary condition is "strong enough".
Necessary conditions exist for failure (debugging assistance).
Sufficient conditions exist for success.
Safety can only be guaranteed by a sufficient condition.
DbC is about success, not about failures.

Regards,

- damien

damien.guichardwanadoo.fr wrote:

> Nothing can be guaranteed by a necessary condition.

True. But it is the user who is doing the guaranteeing by satisfying the
precondition, not the other way around. The user's behaviour is
sufficient if it satisfies the precondition.

Whether a precondition is viewed as necessary or sufficient depends on
whether you are a developer or a user.

To a developer, a precondition can be prepared which is at least strong
enough to guarantee the assumptions the developer is relying on. So, a
precondition is a sufficient condition for correct operation of the
routine it is guarding. The precondition implies correct operation.

To a user, a precondition is a necessary condition, a condition that the
user must meet or exceed. Correct invocation implies the precondition.

Dijkstra (Hoare also, probably) spoke of the weakest precondition
required to achieve the postcondition. In other words, weakening
(widening) the condition brings it closer to the necessary (minimum)
condition.

When talking about "require else" we mean that extra computation has
been provided which caters for an even weaker precondition than was
achievable without it.
--
Peter Horan                     School of Information Technology
peter@deakin.edu.au             Deakin University
+61-3-5227 1234 (Voice)         Geelong, Victoria 3217, AUSTRALIA
+61-3-5227 2028 (FAX)           http://www.cm.deakin.edu.au/~peter

-- The Eiffel guarantee: From specification to implementation
-- (http://www.cetus-links.org/oo_eiffel.html)

> Whether a precondition is viewed as necessary or sufficient depends
> on whether you are a developer or a user.

ok. satisfying the precondition is necessary for invocation and sufficient
for operation.
the precondition is part of the class flat-form, hence the "require" keyword
that emphasizes the user view.

thanks for the clarifications,

- damien