DbC question - duplicated contracts

Hi, I am trying to introduce DbC to our developers (albeit using
Java...one step at a time ! ;) ) ...and am finding that there is
resistance at a certain level, that applying it in what I think is a
rigorous manner is seen as needless, and going too far.

A typical situation is when a function calls a "lower level" function
which does the "real work". It is thought that we are just
duplicating contracts needlessly.

For example, we have various layers in our software - domain,
application, UI, data. At the application level, say, we have
a "store" function (which stores some kind of object to the
database). To achieve its goal, it calls a corresponding data
layer "store" function. The application layer store function
basically does some transforming of the object to an appropriate
format (from a DTO do a domain object), and then calls the data layer
store function.

So, to my way of thinking, the contracts (just concentrating on
postconditions here) are quite straightforward. The application layer
store method will guarantee that the object gets stored. The data
layer store method pretty much also guarantees the same thing. (There
will be various differences too, as well as in the preconditions, eg,
dealing with the different formats).

So, if we have similar postconditions at these 2 levels, it is seen
as pointlessly duplicating them.

However, the way I see it is that is is perfectly ok to do this.
After all, they do in fact do similar things. Also, contracts are for
specifying WHAT is done, not HOW. So, for writing contracts, we
should be oblivious to how the function is fulfilling its
postconditions (in this case by calling the lower level store
function) and simply concentrate on WHAT should be true after the
function has done its job.

Also, "duplicating" the postconditions is building up internal
consistency within the application.

Colleagues are arguing that we should look at what the function is
doing, ie calling the lower level store function, and because it has
the postcondition that it will store the object, then we
should "trust" it to do its job, and not bother duplicating the
postcondition at the application layer.

To me this totally goes against the idea that the contracts are
stating WHAT should be done, not HOW. We might think that it's all ok
now, because we can see that our current implementation calls the
lower level function, but if that changed (perhaps accidently) then
we would never know that the higher level function is not fulfilling
its contract, because we have totally left this out of its contract.

I hope this makes some sense ?
Sorry to have rambled on a bit !

So, can anyone advise me at to how we really should be setting up our
contracts in this kind of situation ?
duplicate, or not ?

thanks very much ! :)



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

Yahoo! Groups Links

<*> To visit your group on the web, go to:
    http://groups.yahoo.com/group/eiffel_software/

<*> Your email settings:
    Individual Email | Traditional

<*> To change settings online go to:
    http://groups.yahoo.com/group/eiffel_software/join
    (Yahoo! ID required)

<*> To change settings via email:
    mailto:eiffel_software-digest@...
    mailto:eiffel_software-fullfeatured@...

<*> To unsubscribe from this group, send an email to:
    eiffel_software-unsubscribe@...

<*> Your use of Yahoo! Groups is subject to:
    http://docs.yahoo.com/info/terms/