In a message dated Fri, 4 Oct 2002, [EMAIL PROTECTED] writes: > On Fri, Oct 04, 2002 at 06:26:31PM -0400, Trey Harris wrote: > > > But what does it mean to be "stronger"? How does Eiffel figure out if > > > a given precondition is "stronger" or "weaker" than another? > > > > Like I said before, boolean logic. Preconditions are OR'd together > > (starting with the deepest subclass and working back to the most ancestral > > class, in order to short-circuit most effectively), postconditions are > > AND'd together (in the opposite order, same reason). > > I can see too many problems with that technique, I think one was > already mentioned where subclasses can unintentionally weaken > preconditions to the point of eliminating them. I'm sort of casting > about looking for another way.
Could you illustrate a case? I don't know what you're talking about. It's completely valid to eliminate a precondition, because "true" is the weakest possible precondition. By definition, an assertion P is weaker than another assertion Q iff Q implies P. Requiring a computer to determine if some condition A, expressed in arbitrary computer code, is weaker than some condition B, also expressed in arbitrary computer code, is unsolvable in the general case and equivalent to the halting problem. So, you either abandon the general case and incorporate a theorem prover into the compiler (!) or you make use of the following theorem: (P or Q) is weaker than Q, because Q implies (P or Q). Trey
