EMCA View of Findler's Contract Flaw Analysis
Peter Horan
>
> Since Dominique and others mentioned their work on Eiffel's EMCA standardization, I was hoping they could comment on whether the recent papers by Robby Findler and Matthais Felleisen [1,2] detailing flaws in the implementation of software contracts in a variety of tools, including Eiffel. These papers are extremely high-quality, and present (IMHO) a compelling case that there are areas in Eiffels contract behavior that need to be addressed.
>
> >From their abstract [1]:
>
> "Because methods may be overridden, it is not sufficient to check
> only pre- and post-conditions. In addition, the contract hierarchy
> must be checked to ensure that the contracts on overridden methods
> are properly related to the contracts on overriding methods. Otherwise,
> a class hierarchy may violate the substitution principle, that is, it
> may no longer be true that an instance of a class is substitutable for
> objects of the super-class."
>
> The papers then describes how Eiffel's DBC mechanisms violate these principals.
I have scanned the paper and attempted to identify the references to how
Eiffel's DBC principles violate these principles.
The examples are entirely in Java. The example in section 5 is most relevant.
The Eiffel code is:
deferred class I
feature
m(a: INTEGER): INTEGER is
require
a > 0
deferred
end
end
------------------
class J
inherit I
feature
m(a: INTEGER): INTEGER is
require else
a > 10
do
end
end
------------------
The argument is that an implementation of m would be faulty were it not to
comply with the original contract.
In other words, an author of class J, IGNORING the inherited precondition
(despite the keyword "else"), but complying with his own restricted precondition
could write faulty code which failed to handle cases in which 0 < a <= 10.
Furthermore, his error would not be detected by precondition checking.
In that an author could do this, it would be helpful for precondition checking
to warn of the failure of the additional precondition when it was masked by the
inherited precondition. Perhaps this should be reported as a routine failure
rather than a precondition failure because it is the implementer's problem, not
the client's.
In the meantime, author's could add check statements for require else clauses in
order to avoid such a problem when using Eiffel.
There is a lot of meat in the paper which I have not read properly. I may have
missed something.
I have not read the second paper and the third reference is only an abstract of
a seminar.
--
Peter Horan School of Information Technology
pe...@deakin.edu.au Deakin University
+61-3-5227 1234 (Voice) Geelong, Victoria 3217, AUSTRALIA
+61-3-5227 2028 (FAX) http://www.cm.deakin.edu.au/~peter
-- The Eiffel guarantee: From specification to implementation
-- (http://www.cetus-links.org/oo_eiffel.html)
Berend de Boer
> In that an author could do this, it would be helpful for precondition checking
> to warn of the failure of the additional precondition when it was masked by the
> inherited precondition. Perhaps this should be reported as a routine failure
> rather than a precondition failure because it is the implementer's problem, not
> the client's.
I didn't get the gist of this paper through the provided abstract. Could
you post a link? Haven't seen the original posting.
One comment: you cannot mask a precondition, preconditions can only be
weakened. So what's wrong with this example? I don't get it. The
implementer specifies that he works in more cases (require else) and
than makes a fault in his implementation.
Looks to me as the kind of bugs I write every day, but hopefully fix at
the end of the day, i.e. nothing abnormal. We all make faults in our
implementation. I don't see the relation with DbC. You can shoot
yourself in the foot with Eiffel, if you force it to. Eiffel doesn't
shoot you in the foot.
--
Quote of the day:
<aleitner_> and when it comes to r/r and s/r, i'll go for s/r anytime
Regards,
Berend. (-:
Andrew Feldstein
OOPSLA 2001 Findler, Felleisen
Contract Soundness for Object-Oriented Languages
for which I found this link on Robby Findler's website:
http://www.ccs.neu.edu/scheme/pubs/#oopsla01-ff
Andrew Feldstein
Eiffel, and insofar as it is applicable to Eiffel, it misunderstands
it.
Specifically, as previously pointed, out, in Eiffel a conforming
class's redefinition of a feature can only weaken its precondition.
Thus, the example cited in the original post (which comes from Section
5 of the paper cited) is bad Eiffel in that Class J's precondition to
"m" *strengthens* the precondition inherited from Class I. I.e., J's
"m" accepts a smaller class of "a" values--1 through 10 are no longer
allowed.
This *would* be a problem if an actual Class J object were passed
polymorphically by a routine believing it had a true Class I object,
and thus only needed to ensure that "a" was more than 0 (not more than
10).
This leaves open the cases where there is an actual weakening of the
precondition in the inheriting class's routine, but the routine fails
to handle the additional possibilities. For example, suppose Class
J's "m" had a precondition that "a" be greater than *or equal* to 0,
but then failed properly to handle the additional possibility, namely
that a could equal 0. This would be just a plain old aphid (that is,
your garden-variety bug).
The only solution to this, assertion-wise, is not to permit the
precondition to change at all. And that would suck.
Or, we could invent a programming language in which bugs simply
weren't permitted.
Peter Horan
Yes.
Peter Horan
>
> This paper although rigorous, seems to be of slight relevance to
> Eiffel, and insofar as it is applicable to Eiffel, it misunderstands
> it.
I posted a reply to a smarteiffel mailing list message to comp.lang.eiffel
(probably where it should be).
Briefly, a precondition in a child class which strengthens an inherited
precondition (not possible in Eiffel) can lead a developer to write the body
consistent with the stronger precondition. Precondition and code taken together,
the code is not substitutable for the parent code. Because it is masked, it will
not throw an exception and identify this.
The basic conclusion is that in practice, this is not a major problem in Eiffel.
Berend de Boer
Yes, and have the paper in the mean-time.
I think it's telling that the words strengthening and weakening do not
appear in the paper.
As I only scanned the paper, can anyone tell me if they really have
missed it or if they just used different words?
If they reall missed it, they've reinvented the wheel.
--
Live long and prosper,
Berend de Boer