Re: Redefine to make a contract stronger (Was: is_equal of HASHABLE)

Frank Boehme wrote:

> But what if we redefine an *effective* feature for the sole purpose to
> make the contract stronger...
> class C
> inherit A B

This works already. Just write:

   class C
   inherit
      A
      B undefine f end
   end

C will get f's postcondition "and-ed" from both A and B, as you would
expect.

Or, if you know that the only purpose of B is to strengthen the
postcondition of 'f', you can write B like this:

   class B
   inherit
      A undefine f redefine f end
   feature f: STRING is
      deferred
      ensure
         result.has_some_property
      end
   end

In that case, there's no need to "undefine f" in class C, because the
concrete version inherited from A will "effect" the deferred version
inherited from B. Again, all ancestral postconditions will be "and-ed"
in C.

> But I am not proposing how this could be added to, errrrm...
> the SmartEiffel.. ahmmm language(?).

Luckily, it turns out that it's already there.

Regards,
-- 
Roger Browne <[email protected]>