Re: Curl, multiple inheritance, and interfaces (was Re: cheerful static typing)

["Kevin Wells" <address@hidden>]

Thanks for the clarification and the references. I just skim read them and
take your point.

Kevin
----- Original Message -----
From: "Robert Bruce Findler" <robby@cs.rice.edu>
To: "Brent Fulgham" <brent.fulgham@xpsystems.com>; "Kevin Wells"
<kevin@ethossoft.co.nz>
Cc: <ll1-discuss@ai.mit.edu>; <matthias@ccs.neu.edu>
Sent: Saturday, January 12, 2002 3:50 PM
Subject: RE: Curl, multiple inheritance, and interfaces (was Re: cheerful
static typing)


> Quoting "Brent Fulgham":
> > I thought that Eiffel used the same covariant rule for enforcing
> > contracts as your paper identified as the correct mode of operation.
> > The various Java implementations you cite *don't* enforce this
> > behavior, which is where the problem lies.
>
> Nope, Eiffel got it wrong, too.
>
> Quoting "Kevin Wells":
> > Eiffel requires that preconditions and postconditions are weakened and
> > strengthened appropriately in descendant classes. Isn't this taking the
> > hierarchy into account?
>
> Yes, but incorrectly.
>
> Eiffel rewrites the programmer's contracts on overridding methods in
> such a way that guarantees that every subtype is a behavioral subtype.
> That is, the re-written program has the property that pre- and
> post-conditions are weakened and strengthened appropriately, *even if
> the original pre- and post-conditions weren't*.
>
> This means that contracts are mis-enforced. In particular, blame for
> contract violations can be assigned to innocent parties, delayed, or
> even missing entirely!
>
> Here is an abstract explanation of what happens (for a more concrete
> one, with more details, let me refer you to the two papers cited at the
> end of this message).
>
> Imagine classes C and D (I will use Java+iContract syntax, but this is
> all also true of Eiffel):
>
>   class C {
>     public void m(...) { ... }
>       @pre {C_precondition}
>   }
>
>   class D extends C {
>     public void m(...) { ..
>       @pre {D_precondition}
>   }
>
> This code-snippet says that C's method `m' has pre-condition
> C_precondition and D's (overriding) method m has pre-condition
> D_precondition. According to Liskov and Wing's, America's, and Meyer's
> work on behavioral subtyping, this means that as the method `m' is
> called, this logical implication:
>
>   C_precondition => D_precondition
>
> must hold (when the pre-conditions are evaluated), or else D is not a
> behavioral subtype of C.
>
> But, instead of checking that, Eiffel rewrites the contracts during
> compilation and acts as if the programmer had written this program:
>
>   class C {
>     public void m(...) { ... }
>       @pre {C_precondition}
>   }
>
>   class D extends C {
>     public void m(...) { ..
>       @pre {C_precondition || D_precondition}
>   }
>
> and Eiffel checks the contracts in this program. If you look closely at
> this program, you'll see that the revised logical implication is this:
>
>   C_precondition => C_precondition || D_precondition
>
> which is a tautology! (and therefore not checked)
>
> Even though the re-written program is always okay, the original one
> isn't -- that's how the contract checker can make all of those mistakes
> I mentioned earlier.
>
> The following papers explain this in more detail. The first talks about
> how to implement contract checking properly and some issues related to
> that. The second's introductory example is clearer than the first's
> (also clearer than the above, but longer) and it makes a first step in
> a contract soundness theory in the spirit of a type soundness theory.
>
>   Findler, Latendresse, Felleisen.
>   FSE 2001
>   Behavioral Contracts and Behavioral Subtyping
>   http://www.cs.rice.edu/CS/PLT/Publications/#fse01-flf
>
>   Findler, Felleisen.
>   OOPSLA 2001
>   Contract Soundness for Object-Oriented Languages
>   http://www.cs.rice.edu/CS/PLT/Publications/#oopsla01-ff
>
> Robby
>