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