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

Hi again,

This discussion brings up a related problem:

Currently a class may only conform to another via more than one path of
conformance if there is no ambiguity in the definition of non-deferred
features, i.e there might be multiple deferred versions being inherited
but not more than one non-deferred version. All inherited post- and
preconditions are added to the contract. Is that correct?

But what if we redefine an *effective* feature for the sole purpose to
make the contract stronger, just as in my intitial proposal for
{HASHABLE}.is_equal? There would be no problem with multiple pathes of
conformace, even though more than one effective version is inherited.
And I think allowing this somehow would be useful (at least for me).

Consider this:

class A
feature f: RES is
   do
      some_instructions;
   end
end

class B
inherit A redefine f end
feature f: RES is
   do
      Result := Precursor
   ensure
      Result.has_some_property
   and

class C
inherit A B
...

This does not look very useful but C could inherit from A and/or B
non-directly via other classes. So we inherit two effective versions of
f which are not identical which is currently forbidden. But there would
be no problem at all. Just add the postcondition. The thing is,
'redefine' is not always used to really re*define*. Actually, I believe
there are many real-world examples where allowing this would be very
helpful. But I am not proposing how this could be added to, errrrm...
the SmartEiffel.. ahmmm language(?).

Regards,

Frank

-- 
Dr Frank Boehme                      | Email: [email protected]
National University of Ireland, Cork | phone: +353-21-4903163
Dept of Computer Science             |   fax: +353-21-4903113
Cork, Ireland                        |

Did you know that if you play a Windows XP cd backwards, you
will hear the voice of Satan?
That's nothing! If you play it forward, it'll install Windows XP.