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.)

Answer tomorrow.

Regards,

Roger

--

--

-- Roger Browne, 6 Bambers Walk, Wesham, PR4 3DG, UK | Ph 01772-687525

-- Everything Eiffel: http://www.*-*-*.com/ | +44-1772-687525