On Friday, October 4, 2002, at 06:23 PM, [EMAIL PROTECTED] wrote:
> On Fri, Oct 04, 2002 at 09:13:45AM -0400, Chris Dutton wrote:
>>> How exactly does one "weaken" a precondition?
>>
>> At least in Eiffel, if you redefine a method, you may not give it
>> stringer preconditions than the original method, but you may have
>> stronger postconditions. In essence, you're not requiring any more of
>> the client, but you can ensure more to them on completion, thus
>> maintaining the parent's contract.
>
> But what does it mean to be "stronger"? How does Eiffel figure out if
> a given precondition is "stronger" or "weaker" than another?
Perhaps an example is the best way to demonstrate this:
class FOO
creation make
feature
make(input: SOME_OTHER_CLASS) is
require
input /= Void
do
-- something here
ensure
input /= Void
end
end
-- Good:
class BAR
inherit FOO redefine make end
creation make
feature
make(input: SOME_OTHER_CLASS) is
-- no requirements, weaker precondition
do
-- yada yada
ensure
input /= Void
old input.some_attribute /= input.some_attribute
-- stronger postcondition is ok.
end
end
-- Bad:
class BAR
inherit FOO redefine make end
creation make
feature
make(input: SOME_OTHER_CLASS) is
require
input /= Void
input.some_attribute = 1
-- requiring more than the parent's make procedure is bad.
do
-- yada yada
-- Not ensuring anything to the client is bad.
-- The parent honored that in its contract, so
-- the child must also.
end
end
