weigand@kub.nl (Hans Weigand) (03/05/91)
Can anybody tell me why Eiffel takes preconditions to be sufficient? Some time ago I asked the reason for Eiffel having *sufficient* preconditions for its methods. I was prompted to this question by the discussion on the inheritance of "add_vertex" from "polygon" to "rectangle", and the various awkward solutions proposed. It is much more natural and logically cleaner to interpret the preconditions as *necessary*. Then there is no problem in adding more preconditions at a lower class. Assuming this lower class is delivered separately, it is reasonable to allow the programmer to negotiate extra conditions. There seems to be only one problem with this approach, and that is that knowing necessary conditions does not give us yet the sufficient conditions. Intuitively, we would like some implicit closure, so that the total of necessary conditions, at compilation time, is taken as the sufficient condition. Logically, this requires a circumscription operation on the precondition predicate. Although this introduces certain non-monotonic behaviour (adding a precondition invalidates the current sufficient condition), it is not a real problem. The add_vertex problem can be solved then by either adding an extra necessary precondition to add_vertex at rectangle level, amounting to "false", so that add_vertex cannot be executed for rectangles, or by leaving the precondition as it is and changing the body in such a way that the rectangle is transformed into a polygon. The choice depends on the requirement definition. The first solution, adding the precondition "false", or, what is the same, "forbidding" add_vertex for rectangles, does not break the contract for the superclass "polygon", because the client is not obliged to use the new subclass "rectangle". But if he wants to use it, he must take it part and parcel. --- Hans Weigand Tilburg University weigand@kub.nl