Re: Design by Contract (was Re: Interesting thread in comp.lang.eiffel)

[David Kristola <David95037@See-My.Sig>]

On Thu, 13 Jul 2000 11:12:53 -0700, Joachim Durchholz wrote
(in message <8kl0r6$2lp6o$1@ID-9852.news.cis.dfn.de>):

> Howard W. LUDWIG <howard.w.ludwig@lmco.com> wrote:
>> David Kristola wrote:
>> 
>>> What kinds of DbC things could i do in Eiffel that i
>>> can't do in Ada with pragma Assert and good typing?
> 
> Stuff like
>   my_parame /= Void

From later in Joachim's post, it is clear that failure to meet
the precondition causes an exception to be raised (at run time,
i assume that a precondition that can be checked at compile time
would be checked, and the code would not compile if it is violated).
Assuming my_parame is an access type, Ada will raise an exception if
it is void (null).

Ada compilers generally give the user the ability to control
the amount of run-time checking compiled in.

> or
>   find_minimum_in (h: HEAP)
>   require
>     not h.is_empty

Depending on the implementation of the heap, this too would
probably cause some sort of exception to be raised if the
heap were empty.

In the past, i had good reason to implement a FIFO queue
that would pop a "dry FIFO" pattern if it were empty.  I
suppose it might be possible to have a heap class that
returns Integer'LAST or Float'LAST when the minimum value
is requested from an empty heap.

> or
>   solve (q: QUADRATIC_EQUATION)
>   require
>     solvable (q)

I know from recent personal experience that a simple 2x2
matrix inversion routine causes an exception to be raised
when the matrix can't be inverted (divide by zero results
in a Constraint_Error to be raised).

Perhaps i am missing something.  If the only way to know
that the precondition is not met is to work the problem
(solve the quadratic equation, in this case) and find
an impass, then what is the difference between writing
it as a precondition vs. writing it as an exception
when the problem can't be solved?

> or
>   sqrt (r: REAL): REAL is
>   require
>     r >= 0.0
> or
>   log (r: REAL): REAL is
>   require
>     r > 0.0
> (try to put both the preconditions for sqrt and log into a range type
> <g>).

Simple.

   subtype None_Negative_Float_Type is Float range 0.0 .. Float'LAST;
   subtype Positive_Float_Type is None_Negative_Float_Type range
      Float'SUCC(0.0) .. Float'LAST;

   function Sqrt(R : Non_Negative_Float_Type) return Float;
   funciton Log(R : Positive_Float_Type) return Float;

As subtypes of Float, i can call either routines with a Float
variable (without using a type cast), and an appropriate
constraint check will be generated by the compiler.  That
check can be eliminated by telling the compiler to not perform
that checking.

In this particular case, i'm not sure what the subtype
constraint check would add.  Very limited cases could be
checked at compile time.  At run time, if the preconditions
are violated, an excpetion will be raised.

> It's just more flexible. In fact Eiffel has no range types; the
> understanding is that contracts properly include them. (Personally, I
> tend to disagree but I can live well with just contracts.)

It seems to me that contracts can add to the code, but i really
like Ada's robust typing capabilities.

> I have used DbC in practice, and it is immensely useful.

I am going to continue looking into DbC as time permits.  I
wonder if there is a free Eiffel compiler available for the
Mac so that i can play around with it.

Thanks,

-- 
--djk, keeper of arcane lore & trivial fluff
Home: David95036 plus 1 at america on-line
Spam: goto.hades@welovespam.com