Eiffel "Gotchas"

07 April 1998

Gotcha #9 - Answer and Explanation

Here's the question again:

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

We have produced the postcondition by repeating the routine body, substituting "=" for ":=". This approach is common, and works in most cases - but not for BOOLEAN expressions. Because "=" has higher precedence than "or", the postcondition is interpreted as:

   ( result = (a and not b) ) or (b and not a)

We need to add an extra pair of parentheses to make our postcondition correct:

   result = ( (a and not b) or (b and not a) )

Thanks to Franck Arnaud for suggesting this one.

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

Eiffel "Gotchas"