On DBC

[Matthew Tuck]

Hans-Dieter.Dreier@materna.de wrote:

> Since the term "Design By Contract" is trademarked, I'd suggest
> to simply use "DBC" for the whole issue.

I usually use "assertions".  =)

> I think DBC is a nice approach to adapt assertions to the OO world
> by making them inheritable and incorporating them into the syntax.
> Properly used, it should help catch a lot of bugs and flawed design
> decisions in a pretty early development stage.
> It also enhances program documentation.
> If the documentation is checked by the compiler rather than being
> a mere comment, it is much more trustworthy.

Yep.

> I'm not sure, however how far the enforcement of assertions by the
> Eiffel compiler really goes. I got the impression that it relies on
> inserting runtime checks rather than doing a static analysis
> at compile time.

This is purely an implementation issue.  All the language does is make
it flexible.  Hence while it is certainly an issue, it's one that
doesn't
need to be solved early.

> This has serious disadvantages:
>
> 1. Runtime penalty, which may be quite severe if often used low level
> classes do extensive DBC checking.
>
> 2. DBC violations are only caught at runtime if and when they occur.
> Having them reported at compile time would be far better.
> It's the same as having dynamic type checking instead of
> static type checking.

If you consider assertions as if statements, the analysis many compilers
do for advanced checking and optimisation solves both of these problems.
There's no runtime penalty if it can be optimised out.  There's a
compile time warning if it can be determined the assertion will always
raise an exception.

> invariants:     a                       // a does not change

This is usually expressed as something like "old(a) = a" but we could do
a shorthand like "same(a,b,c)".

> You see, given the proper background information,
> it is not only possible to automatically derive preconditions,
> but also to prove termination and the fact that the result
> may not be greater than either of the parameters.
> At least in an example as simple as this one.

Program proving and generation are pretty much the holy grails of
computing.  They are a huge Pandora's box that I would have to start
another project for.  Plus I don't know enough about them!

Generating assertions is an interesting idea.  It would be similar to
type derivation systems.

> I think that a partial approach might be feasable, however.
> And who knows, eventually we might be able to extend it to cover parts
> of the more complicated cases.

Well it's certainly possible, and in a total environment some proving
utilities would be handy.

> This would allow to eliminate checks for those cases where the value to
> be tested is a constant known at compile time.

This is actual pretty standard optimisation practice (at least some
check elimination is).

> These cases include all type checking in a strongly typed language, for
> example.  I like the idea to view type checking as a part of a more
> general concept, looking at types as a partially ordered collection of
> constants (reflecting the inheritance hierarchy).

Essentially you'd be interested in three things - type, implementation
and state.  These could all vary pretty independently, although they are
interwoven.

-- 
     Matthew Tuck - Software Developer & All-Round Nice Guy
             mailto:matty@box.net.au (ICQ #8125618)
       Check out the Ultra programming language project!
              http://www.box.net.au/~matty/ultra/