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

[Robert Bruce Findler <address@hidden>]

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