require, ensure, and Design by Contract 
Author Message
 require, ensure, and Design by Contract

Hi Ruby people,

currently, I am reviewing the forthcoming Ruby book of Dave and Andy.
Some time ago, Andy told me, he planned to add direct support for Design
by Contract to Ruby. As a convonced Eiffelist, furthermore working for
the company, where Eiffel has its origin :-), I would like a Design by
Contract support in Eiffel very much.

Sadly, I discovered though that two of the "classic" DbC keywords,
"require" and "ensure", already have another meaning in Ruby. Are there
currently any plans to add Design by Contract support to Ruby? If yes, I
would likke to give some input.

--
Best regards,
Patrick

--
---------------------------------------------------------------------------

                  URL: http://www.*-*-*.com/

     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
        >Hi Ruby people,
        >
        >currently, I am reviewing the forthcoming Ruby book of Dave and Andy.
        >Some time ago, Andy told me, he planned to add direct support for Design
        >by Contract to Ruby. As a convonced Eiffelist, furthermore working for
        >the company, where Eiffel has its origin :-), I would like a Design by
        >Contract support in Eiffel very much.
        >
        >Sadly, I discovered though that two of the "classic" DbC keywords,
        >"require" and "ensure", already have another meaning in Ruby. Are there
        >currently any plans to add Design by Contract support to Ruby? If yes, I
        >would likke to give some input.

I've been threatening to implement such a beast for some
time; as soon as I have a free minute I'm still hoping to
get to it.  I agree that it could be an important feature
and good selling point for Ruby.

Yes, the Eiffel style keywords have already been used.
In the few trial versions I've put together, I used
"pre" and "post" as the keywords, in addition to
an "invariant" method and a simple "check".

I believe that DbC can be added purely as an add-on in Ruby,
that no interpreter changes will be necessary -- Matz
is busy enough as it is, I'd rather not burden him with
anything extra if I can help it :-)

Perhaps I can carve out some time this week to give it
another look...

/\ndy

--
Andrew Hunt, The Pragmatic Programmers, LLC.
Innovative Object-Oriented Software Development

--
Our New Book: "The Pragmatic Programmer" Published by Addison-Wesley Oct 1999
              (see www.pragmaticprogrammer.com/ppbook)
--



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
On Sun, 9 Jul 2000 10:27:24 -0400,

Quote:

>I've been threatening to implement such a beast for some
>time; as soon as I have a free minute I'm still hoping to
>get to it.  I agree that it could be an important feature
>and good selling point for Ruby.

Well, Andy, let's not forget our "other project" though. ;-) (Sorry
newsgroup, inside hunt...aehhh...hint *g*).

Quote:
>Yes, the Eiffel style keywords have already been used.
>In the few trial versions I've put together, I used
>"pre" and "post" as the keywords, in addition to
>an "invariant" method and a simple "check".

How about loop invariants? Loop variants are not really needed in Ruby,
as far as I overlook it.

Furthermore, it must be possible to select different levels of assertion
monitoring. And what about a tool to display the "short from", "flat form",
and "flatshort form" of a class?

--
Best regards,
Patrick

--
---------------------------------------------------------------------------

                  URL: http://www.geocities.com/Vienna/5357/

     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
Patrick,

I'm interested in this, too. I've been trying to
put something together, but my Ruby is not
(yet!) as good as Dave's.

I'd like to have an implementation that puts as
little burden on the programmer as possible.
Therefore I'm shying away from what I'm looking
at right now: An implementation that requires the
programmer to define two other methods for each
method for which he wants to check pre- and post-
conditions.

I thought there might be some way to generate
these on the fly, at the time the "pre" function was
called, for instance. But there is no way to determine
the class or object of the method that called you.

But I have been thinking of a syntax something like
this:

   pre("positive:x>0  empty:arr.size==0  old.somevar")
   # ...
   post("nonempty:arr.size>0  incr:somevar=old.somevar+1")

The "label:" notation would provide a mnemonic for the
error message. (Doesn't Eiffel provide this?)

The "old.somevar" notation would be a signal to save off the
value of somevar so that it could be checked at the end.

This is all extremely half-baked, though. Inheritance is the real
issue: We have to make sure that contracts are heritable.

Discussion is welcome.

Hal Fulton



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract

Quote:
> I thought there might be some way to generate
> these on the fly, at the time the "pre" function was
> called, for instance. But there is no way to determine
> the class or object of the method that called you.

True, but you _can_ determine:

  1.  all the methods in the current class
  2.  when any methods are _added_ to a module
  3.  the current subclasses of a class
  4.  when a class or module is used to extend another

Using these combinations, I _think_ there's enough power to be able to
wrap existing methods in pre- and -post condition handlers (where the
post-condition handler also checks the class invariant), and to be
able to perform the wrapping on subclasses when needed. That was the
approach I was considering.

Quote:
> The "old.somevar" notation would be a signal to save off the
> value of somevar so that it could be checked at the end.

The problem I bumped in to here was saving away parameters to the
method being called. For example, in

    def incr(n)
      n + 1
    end
    { post: result == n.old + 1 }

I couldn't see a way to determine that 'n' was a parameter. Apart from
this problem, I agree with Andy that DbC could be added with no
interpreter mods.

Regards

Dave



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
On Sun, 9 Jul 2000 14:36:44 -0700,

Quote:
>I'd like to have an implementation that puts as
>little burden on the programmer as possible.
>Therefore I'm shying away from what I'm looking
>at right now: An implementation that requires the
>programmer to define two other methods for each
>method for which he wants to check pre- and post-
>conditions.

Agreed.

Quote:
>I thought there might be some way to generate
>these on the fly, at the time the "pre" function was
>called, for instance. But there is no way to determine
>the class or object of the method that called you.

This is a problem, yes.

Quote:
>But I have been thinking of a syntax something like
>this:

>   pre("positive:x>0  empty:arr.size==0  old.somevar")
>   # ...
>   post("nonempty:arr.size>0  incr:somevar=old.somevar+1")

I quite dont like the fact that you write the assertions "horizontally".
It is quite hard to read. I would prefer a  "pre" statement and then
list all assertions, one per line. This would be more readable.

Quote:
>The "label:" notation would provide a mnemonic for the
>error message. (Doesn't Eiffel provide this?)

Yes it does.

Quote:
>The "old.somevar" notation would be a signal to save off the
>value of somevar so that it could be checked at the end.

Basically, I agree. But I do not like "old" has to be mentioned in
"pre". This only would cause stupid ommission errors.

Quote:
>This is all extremely half-baked, though. Inheritance is the real
>issue: We have to make sure that contracts are heritable.

..and we need something to make the programmer aware of that he is
weakening preconditions/strengthening postconditions in a subclass. In
Eiffel, this is done by enforcing "require else" and "ensure then" in a
subclass for adding assertions.

--
Best regards,
Patrick

--
---------------------------------------------------------------------------

                  URL: http://www.geocities.com/Vienna/5357/

     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------



Thu, 26 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
On 09 Jul 2000 16:17:44 -0500,

Quote:

>Using these combinations, I _think_ there's enough power to be able to
>wrap existing methods in pre- and -post condition handlers (where the
>post-condition handler also checks the class invariant), and to be
>able to perform the wrapping on subclasses when needed. That was the
>approach I was considering.

In Eiffel, invariants are checked before *and* after the execution of an
*exported* routine (no invariant checking for private routines!). I do
not have the rationale available in my mind right now ;-), but it is
clearly discussed in OOSC2.

Quote:
>I couldn't see a way to determine that 'n' was a parameter. Apart from
>this problem, I agree with Andy that DbC could be added with no
>interpreter mods.

In general, I agree, too. But I see many obstactes to this:

        - Inheriting assertions.

        - Enforcing that pre-/postconditions are weakened/strengthened in a
          subclass by enforcing the use of another keyword.

        - Convenient implementation of "old" expressions.

        - Recursive assertions. If "pre" or "post" calls a feature that
          returns a boolean and that itself has a "pre" and/or "post", these
          contracts are *NOT* checked.

--
Best regards,
Patrick

--
---------------------------------------------------------------------------

                  URL: http://www.geocities.com/Vienna/5357/

     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------



Fri, 27 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
Dave:

Quote:
> True, but you _can_ determine:

>   1.  all the methods in the current class
>   2.  when any methods are _added_ to a module
>   3.  the current subclasses of a class
>   4.  when a class or module is used to extend another

I'm not going to try my wings with this one, but I thought about it (too)
and assumed that the basic DBC should be quite possible thing to do once we
have a hook in the interpreter for adding methods. I didn't know we have
such hook already. But just as Dave writes at 2., the beast exists already.

The (from the top my head) example what replacing could do.

Quote:
> Using these combinations, I _think_ there's enough power to
> be able to
> wrap existing methods in pre- and -post condition handlers (where the
> post-condition handler also checks the class invariant),

Me too.

Quote:
> and to be
> able to perform the wrapping on subclasses when needed.

Could you say what's the need here? Why do we have to wrap them?

Quote:
>     def incr(n)
>       n + 1
>     end
>     { post: result == n.old + 1 }

What if the post is real method and working like my example later? Can't we
pass the copy of the arguments? (Probably not, because it leads to some
other weird problems... But even so, I don't follow you here.

Patrick:

Quote:
> In Eiffel, invariants are checked before *and* after the
> execution of an
> *exported* routine ...
> I do not have the rationale available in my mind right now ;-),

Neither do I. Assuming there's no side-effects and we check the invariant
after each call, I can't see how the object could be in invalid state when
we enter the method. Well, anyway it's just an optimization to rip off the
invariant check before precondition check. (And Ruby will allow weird
side-effects quite probably, it's up to developer whether to mess around :).

Quote:
>    - Inheriting assertions.

Should be no problem. Unless you're talking about something else than:

  class Foo
    def invariant
      raise "always wrong (for example, Foo is a 'abstract' base class"
    end
  class Bar < Foo
    def foo
      puts "foo"
    end
  end

  # Bar.new.foo  # raises invariant error at Foo

  class Bar
    def invariant
      # raise "would raise, but we're not in abstract base class anymore :)"
    end
  end

  Bar.new.foo  # should print "foo"

Quote:
>    - Enforcing that pre-/postconditions are
> weakened/strengthened in a
>      subclass by enforcing the use of another keyword.

I'm not sure we're really implementing full-scale Eiffel-type of DBC here. I
think I saw someone (maybe Dave) saying it's not entirely clear we have need
for automatic invariant since we can always do it explicitly:

  class Foo
    def invariant # as usual
    end
    def pre_foo
      invariant   # call explicitly
    end
    def foo
    end
  end

Anyway, it's not hard to do it implicitly either.

Quote:
>    - Convenient implementation of "old" expressions.

No idea.

Quote:
>    - Recursive assertions. If "pre" or "post" calls a feature that
>      returns a boolean and that itself has a "pre" and/or
> "post", these
>      contracts are *NOT* checked.

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

Anyway, the replacing method could be like following. First real definition
and then what our DBC workaround has created by itself:

  class Foo
    def foo
      puts "foo"
    end
  end

->

  class Foo
    def invariant   # automatically created empty stub
    end

    def pre_foo     # automatically...
    end

    #aliased orig_foo to point foo

    def foo(*args)
      old_args = args.dup

      error = pre_foo(args)
      raise error if error   # or whatever will be the way to signal

      orig_foo(args)

      error = post_foo(old_args)
      raise error if error

      error = invariant
      raise error if error
    end

    def post_foo    # automatically...
    end
  end

And then we can add the check for no checking recursion by changing the core
of 'foo' a little bit.

      if $DBC_recursion == 0
        $DBC_recursion += 1

        error = pre_foo(args)
        raise error if error   # or whatever will be the way to signal

        orig_foo(args)

        error = post_foo(old_args)
        raise error if error

        error = invariant
        raise error if error

        $DBC_recursion -= 1
      end

This is not going to work with multithreading, but what works ;?). I think
this is displaying clear need for thread-wide global area, and maybe there's
already such thing but I'm just an ignorant developer :).

        - Aleksi



Fri, 27 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract

Quote:

> > and to be
> > able to perform the wrapping on subclasses when needed.

> Could you say what's the need here? Why do we have to wrap them?

To enforce contracts on their methods.

Quote:
> >     def incr(n)
> >       n + 1
> >     end
> >     { post: result == n.old + 1 }

> What if the post is real method and working like my example later?
> Can't we pass the copy of the arguments? (Probably not, because it
> leads to some other weird problems... But even so, I don't follow
> you here.

The expression uses a variable 'n', but we can't tell what 'n' is: we
can guess that it's a parameter, but there is no reflection mechanism
that gives you the names and positions of a parameter, so the wrapper
can't synthesize it.

Quote:
> I'm not sure we're really implementing full-scale Eiffel-type of DBC
> here. I think I saw someone (maybe Dave) saying it's not entirely
> clear we have need for automatic invariant since we can always do it
> explicitly:

That wasn't me. I'm a lazy sod, so I'd use the minimal typing and most
automation available ;-)

Regards

Dave



Fri, 27 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract
On Mon, 10 Jul 2000 14:51:50 +0200,

Quote:

>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

--
---------------------------------------------------------------------------

                  URL: http://www.geocities.com/Vienna/5357/

     Fingerprint: 3C FB B0 A7 E2 C2 3B 2D  68 6C 66 7E B7 D5 C2 70
---------------------------------------------------------------------------



Fri, 27 Dec 2002 03:00:00 GMT  
 require, ensure, and Design by Contract

Quote:
> > In Eiffel, invariants are checked before *and* after the
> > execution of an
> > *exported* routine ...
> > I do not have the rationale available in my mind right now ;-),

> Neither do I. Assuming there's no side-effects and we check the invariant
> after each call, I can't see how the object could be in invalid state when
> we enter the method. Well, anyway it's just an optimization to rip off the
> invariant check before precondition check. (And Ruby will allow weird
> side-effects quite probably, it's up to developer whether to mess around :).

Consider an object that needs to make a transition from state A to
state B, but has to do a non-trivial amount of work to make the
transition.  So it calls a bunch of internal methods that tweak the
state until finally we arrive at B. While we're executing these methods
our member data may not yet be consistent so any invariant checks will
fail.

I ran into these sorts of problems with my first cut at DBC in C++.
They're pretty annoying: if all methods check the invariant you wind up
having to significantly weaken your invariant.

  -- Jesse



Thu, 02 Jan 2003 03:00:00 GMT  
 
 [ 11 post ] 

 Relevant Pages 

1. Difference between require and ensure just syntactic sugar?

2. redefining require and ensure clauses

3. Beyond assert-- require, ensure Eiffelisms

4. Newbie: Ensuring a Required Argument for Constructor?

5. 10 SMALLTALK VISUALWORKS DEVELOPERS REQUIRED - Contract 18 months

6. SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

7. SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

8. 6 SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

9. SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

10. 6 SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

11. 6 SMALLTALK VISUALWORKS/VISUALAGE DEVELOPERS REQUIRED - Contract 16 months TORONTO AREA

12. SMALLTALK DEVELOPERS URGENTLY REQUIRED - Contract and Permanent-

 

 
Powered by phpBB® Forum Software