mrilu <mrilu / ale.cx> writes:

> Me too! I've thought about usefulness of invariants and method conditions
> and tried to find imagine why they are more usefull than normal
> assertions. I don't know. I guess since they are named a little bit
> differently they could be used as a part of the documentation. And there I
> can see their usefulness easily.

There are a couple of things about DBC that make it both incredibly
useful and also hard to implement:

1. Pre- and post-conditions apply both to a method and to anyone that
   overrides that method. So, for example, Object.to_s might have a
   post condition that the return value must be a String. If we have

     class Fred
      def to_s
       return 3
      end
     end

   This will trigger a failure in Object.to_s's postcondition

2. You must be able in the postcondition to access the values of
   variables as they were on entry to the method. For example

   def addOneTo(aValue)
    aValue += 1
    return aValue   # contrived, I know
    post { return = aValue.orig + 1 }
   end

   The notation here is arbitrary, it's the concept I'm trying to get
   across.

We know how to do (1) from within Ruby (that is by writing just Ruby
code). We haven't worked out how to do (2) yet...


Dave