Eiffel "Gotcha" #9 - postconditions
Author Message
Eiffel "Gotcha" #9 - postconditions

Suppose we have this function:

area(x, y: REAL): REAL is
do
result := x * y
end

It's quite common to add a postcondition obtained from the body by
replacing ":=" with "=", like this:

area(x, y: REAL): REAL is
do
result := x * y
ensure
result = y * y
end

At first glance, this postcondition may seem like a waste of time, but its
usefulness is in conjunction with inheritance. The postcondition can catch
bugs in descendants. A descendant may redefine a routine to obtain its result
by a different algorithm, or from storage instead of by computation, in which
case the postcondition ensures that the result match the original one.

Here's another example of this same approach. Where's the bug?

exclusive_or(a, b: BOOLEAN): BOOLEAN is
do
result := (a and not b) or (b and not a)
ensure
result = (a and not b) or (b and not a)
end

(Suggested by Franck Arnaud.)

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.*-*-*.com/ | +44-1772-687525

Sun, 07 Nov 1999 03:00:00 GMT
Eiffel "Gotcha" #9 - postconditions

Quote:
>     ensure
>       result = y * y

Sorry, this should have been "x * y". This error was in the example; the
question part is OK as it stands.

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525

Sun, 07 Nov 1999 03:00:00 GMT
Eiffel "Gotcha" #9 - postconditions

Quote:

> Here's another example of this same approach. Where's the bug?

>   exclusive_or(a, b: BOOLEAN): BOOLEAN is
>     do
>       result := (a and not b) or (b and not a)
>     ensure
>       result = (a and not b) or (b and not a)
>     end

> (Suggested by Franck Arnaud.)

The intended meaning of the post condition is:
result = ( (a and not b) or (b and not a) )

However, since the type of result is BOOLEAN and the operator precedence
of "=" is higher than that of "or" (6 vs 4 (ETL2 p377)) the postcondition
is interpreted as:
( result = (a and not b) ) or (b and not a)

which is not the same as what is wanted.

Just this sort of thing has caught me out a number of times in the past.
May be there is a case for introducing an equivalence operator (of lower
precedence than "implies") into the language? Even QBasic has one.

-----------------------------------------------------------------------

Sun, 07 Nov 1999 03:00:00 GMT
Eiffel "Gotcha" #9 - postconditions

Quote:

> Here's another example of this same approach. Where's the bug?

>   exclusive_or(a, b: BOOLEAN): BOOLEAN is
>     do
>       result := (a and not b) or (b and not a)
>     ensure
>       result = (a and not b) or (b and not a)
>     end

> The intended meaning of the post condition is:
>        result = ( (a and not b) or (b and not a) )

> However, since the type of result is BOOLEAN and the operator precedence
> of "=" is higher than that of "or" (6 vs 4 (ETL2 p377)) the postcondition
> is interpreted as:
>        ( result = (a and not b) ) or (b and not a)

> which is not the same as what is wanted.

Ian has said it all!

Quote:
> Just this sort of thing has caught me out a number of times in the past.
> May be there is a case for introducing an equivalence operator (of lower
> precedence than "implies") into the language? Even QBasic has one.

How would you improve on the Eiffel precedence? The pattern in this
"Gotcha" is much less common than the following pattern, which is handled
correctly without parentheses:

x = 5 and y = 6

I find Eiffel's precedence very natural. How does QBasic handle these two
cases?

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525

Mon, 08 Nov 1999 03:00:00 GMT
Eiffel "Gotcha" #9 - postconditions

Quote:
>Just this sort of thing has caught me out a number of times in the past.
>May be there is a case for introducing an equivalence operator (of lower
>precedence than "implies") into the language? Even QBasic has one.

My news reader has lost Roger's answer to the gotcha since last night
and so I don't have a copy to consult. I do remember his asking further
about how the equivalence operator would work.

I was thinking of the introduction of an _additional_ boolean operator to
Eiffel. This would be the binary boolean operator equivalence which
corresponds to the equivalence operator found in classical propositional
logic - just as "and", "or" and so on of Eiffel correspond to the
conjunction, disjunction and so on operators of classical propositional
logic. The Eiffel "=" operator would remain the same.

I was careful to use the sentence form "May be ... ?" when making the
suggestion since I am aware of the caution required when proposing a
language extension - see ETL2 p507 for Dr Meyer's heartfelt views.
Especially so in this case, since the operator is a "convenience"
operator and the same effect can be obtained by using "=" and parentheses.

-----------------------------------------------------------------------

Tue, 09 Nov 1999 03:00:00 GMT
Eiffel "Gotcha" #9 - postconditions

Quote:

> I was thinking of the introduction of an _additional_ boolean operator to
> Eiffel. This would be the binary boolean operator equivalence which
> corresponds to the equivalence operator found in classical propositional
> logic - just as "and", "or" and so on of Eiffel correspond to the
> conjunction, disjunction and so on operators of classical propositional
> logic. The Eiffel "=" operator would remain the same.

> I was careful to use the sentence form "May be ... ?" when making the
> suggestion since I am aware of the caution required when proposing a
> language extension - see ETL2 p507 for Dr Meyer's heartfelt views.
> Especially so in this case, since the operator is a "convenience"
> operator and the same effect can be obtained by using "=" and parentheses.

Very wise. I'm afraid I sometimes err on the side of brashness in the same
situation, but Usenet soon puts me straight!

Although an equivalence operator would resolve Gotcha #9, it would introduce
a whole new class of Gotchas, where one uses the wrong kind of equality test
by mistake.

In any case, if I can remember to use the low-precedence equivalence operator,
I am just as likely to remember to use "=" and parentheses.

Regards,
Roger
--
--
-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525
-- Everything Eiffel: http://www.eiffel.demon.co.uk/ | +44-1772-687525

Tue, 09 Nov 1999 03:00:00 GMT

 Page 1 of 1 [ 6 post ]

Relevant Pages