From: pschoenb@... (Patrick Schoenbach)
Date: 2000-07-10T22:13:05+02:00
Subject: [ruby-talk:03917] Re: require, ensure, and Design by Contract

On Mon, 10 Jul 2000 14:51:50 +0200,
Aleksi Niemel <aleksi.niemela@cinnober.com> wrote:


>Oh, this is new to me. Could you elaborate? Why assertions should not be
>checked?

Ok, let me provide two examples. Since there is no definitive DbC syntax
in Ruby yet, please let me write it in Eiffel.

Imagine, you have a class NUMERIC and an operator "+". then you go on,
and write:

   infix "+" (other: like Current): like Current
      -- Sum with 'other' (commutative).
      require
         other_exists: other /= void
      deferred
      ensure
         result_exists: result /= void
         commutative: equal(result, other + Current)
	  end

..and oops, the postcondition calls operator "+" again. If you would
check assertions recursively, you have an endless recursion here. Of
course, you can say "I would not write such a postcondition" :-), but
such cases can happen more easily than it seems on first look. 

Lets have a look at invariants. Imagine, you have a class CIRCULAR_LIST,
and you write an invariant like:

   previous.next = Current

This would trigger the class invariant check of 'previous', then of its
'previous', etc etc. But also it would trigger another check on
'previous.next', and so on forever.

Is the problem clearer now?

-- 
Best regards,
Patrick

-- 
---------------------------------------------------------------------------
            	  e-mail: pschoenb@solidsoft.iksys.de
                  URL: http://www.geocities.com/Vienna/5357/
 PGP Public Key: Mail to pgp@solidsoft.iksys.de with 'pschoenb' as subject
     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------