Re: Old paper on DbC and ADTs

>>>>> "LEMAITRE" == LEMAITRE Guillaume <[EMAIL PROTECTED]> writes:

    LEMAITRE> I read those slides. What appears to me is that the way
    LEMAITRE> the STACK class is presented is great because you can
    LEMAITRE> prove its behavior, but it is not implementable as
    LEMAITRE> is. Recursion is beautiful for proof but may be very
    LEMAITRE> time and memory consumming for contract checking. That's
    LEMAITRE> what mr McKim says, we have to find a compromise between
    LEMAITRE> both goals. Are there some recipes for coding provable
    LEMAITRE> and efficient classes ?

I also looked at them, but understood that their minus_one query gave
them the ability to prove every feature.

-- 
Regards,

Berend.

  ** you're welcome to the #eiffel irc channel on irc.freenode.net