Eiffel "Gotchas"

07 April 1998

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 = x * 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

ANSWER

Eiffel and NICE are registered trademarks of the Nonprofit International Consortium for Eiffel.

Eiffel "Gotchas"