On DBC

[Hans-Dieter.Dreier@materna.de]

--Hnb6jJ8zVRLOYlv9esRmnY4uDMrBUKMH
Content-type: text/plain; charset="ISO-8859-1"
Content-transfer-encoding: quoted-printable

On DBC
=3D=3D=3D=3D=3D=3D

"Design By Contract"

If someone wants an easy introduction into this topic,
I would recommend to have a look at the following sites:

http://www.eiffel.com/doc/manuals/language/intro/assertions.maker.html
http://www.eiffel.com/doc/manuals/technology/contract/page.html

For an introduction to Eiffel:

http://www.progsoc.uts.edu.au/~geldridg/eiffel/advance-intro/

AFAIK Eiffel still is the reference language for
this sort of semantic checking. =


First, I want to express some general opinions on this topic.

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

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.

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 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.

Then I looked at how static DBC checks could be implemented and quickly
found out that doing a statical analysis is a tough job.
The possible benefits are so great, however, that even a partial statical
analysis could be worth the effort.

Analysis would be done method-wise.
Starting from the preconditions and class invariants it would follow contro=
l
flow, modifying the current set of preconditions as the values involved are=
 changed.

To get a common ground for discussion and a rough idea what we're talking a=
bout,
first a quick sketch how I imagine an analysis could be performed (in princ=
iple),
using a simple example (Greatest Common Divisor, hopefully I got it right):

int GCD (int a, int b) {
if a.mod (b) =3D=3D 0
	return b;
else
	return GCD (b.mod (a), a);
}

where a.mod (b) has the following ...
precondition:   b !=3D 0			// may not divide by 0
postconditions: abs (result) < abs (b)
                (result =3D=3D 0) || (a !=3D 0)// result must be 0 if a =3D=
=3D 0
invariants:     a			// a does not change


At first, there are no preconditions specified for GCD: a and b may take an=
y value.
This is checked against the precondition of the mod call inside the if firs=
t
and a violation is detected: b !=3D 0 is not guaranteed.
The precondition that has been violated must be ANDed to the current condit=
ion
and propagated back (which is easy here because we're still at the start of=
 the program),
forming a precondition b !=3D 0 for GCD. After applying this, we have to st=
art over.
Since the postcondition of mod does not exclude a result of zero, the then-=
path
of the comparison may be executed, yielding a result of b and a postcoditio=
n
of a.mod (b) =3D=3D 0 for that return.
Since the postcondition of mod does not force the result of mod to be zero,=
 the else-path
of the condition may be executed. The current precondition is a.mod (b) !=
=3D 0 for this path.
>From this it follows that a !=3D 0 for the else-path
(see last postconditon of mod: First part of OR is false, so second one mus=
t be true).
Next a call to mod is involved.
The condition for a is tested against the  precondition of mod and no viola=
tion is detected.
The postcondition for this return is hard to determine because of the recur=
sion.

If the inference engine that takes care of all this is really smart,
it can also prove that recursion will terminate because of the first postco=
ndition of mod,
combined with the fact that a and b are swapped for each recursion
so that the postcondition mentioned is applied to each parameter in turn, r=
educing
abs (a) and abs (b) each other turn until the if evaluates to true.

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.

But I'm afraid I won't program a smart prover like the one sketched above.
My head simply is not big enough for this, and life is too short.

Some of the challenges involved are:
1. Determine possible and allowable values of each variable
   and intermediate result.
2. Match possible and allowable value sets.
3. Simplify conditions by omitting superfluous parts.
4. Back-propagation of conditions involves applying the "reverse" of
   the actual operations performed.

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.

If we build an integrated environment, where the compiler, the source,
the runtime system and the program under construction are all stored in obj=
ects
and thus are all accessible (and executable) at compile time, an important =
prerequisite
for statical DBC tests is already there: The compiler can compile assertion
clauses first and then apply them against values it encounters during compi=
lation.
This would allow to eliminate checks for those cases where the value to be =
tested
is a constant known at compile time.
These cases include all type checking in a strongly typed language, for exa=
mple.
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).

What does everyone think of this?

--

Regards,

Hans-Dieter Dreier
(Hans-Dieter.Dreier@materna.de)=

--Hnb6jJ8zVRLOYlv9esRmnY4uDMrBUKMH
Content-type: text/plain; charset="ISO-8859-1"
Content-transfer-encoding: quoted-printable

IDENTIFIKATIONSANGABEN:
a18368a.txt IA5 DX-MAIL X.400 User Agent=

--Hnb6jJ8zVRLOYlv9esRmnY4uDMrBUKMH--