design by contract versus doctest

[aku]

There seems to be a contradictive approach in
these two things. Example: In the doctest documentation
(http://www.python.org/doc/current/lib/module-doctest.html)
a required precondition (i.e. n is an integer and >= 0)
is verified in the function itself:

if not n >= 0:
raise ValueError("n must be >= 0")

But in "design by contract" this responsibility is squarely
on the shoulders of the caller, and is *not* checked in
the function.

I'm confused as to what the "best" approach is.

Isn't it so, that by applying DBC, a lot of unittests can be
made redundant?

shan.

 

[Yermat]

There seems to be a contradictive approach in
these two things. Example: In the doctest documentation
(http://www.python.org/doc/current/lib/module-doctest.html)
a required precondition (i.e. n is an integer and >= 0)
is verified in the function itself:

if not n >= 0:
raise ValueError("n must be >= 0")

But in "design by contract" this responsibility is squarely
on the shoulders of the caller, and is *not* checked in
the function.

I'm confused as to what the "best" approach is.

Isn't it so, that by applying DBC, a lot of unittests can be
made redundant?

shan.

I disagree with you !
Both are needed and not contradictory...

In design by contract, you assume that caller do not call you with
stupid argument. So you can see this precondition as something sure or
as something to check.
In the language that use the most Design by Contract, ie Eiffel, by
default it check those condition on all call and give you something like
and assert Error. (see
http://www.python.org/doc/essays/metaclasses/Eiffel.py for something
similar in python). But when you have finish to write your application
you can compile it without those check because you are sure nobody will
do false check !
Like in python if you optimize byte code (option -O), it delete all
assertions.

Hence there is no contradiction.
And to improve your code, you can (must?) do unittest with, for example,
doctest.

Yermat

 

[Peter Hansen]

Isn't it so, that by applying DBC, a lot of unittests can be
made redundant?

How would you propose verifying that your code will work if you
don't run tests before you ship?

Don't say "manual testing"...

-Peter

 

[aku]

How would you propose verifying that your code will work if you
don't run tests before you ship?

in debugging mode you obviously have to ensure that the caller
makes sure that all preconditions are met...then - by contract -
the postconditions are met on returning from the function.
A very very simple example, but just to make the point:

n = 1
# at this point we are sure that n is an integer and n>=0
result = sort(n)

 

[Peter Hansen]

in debugging mode you obviously have to ensure that the caller
makes sure that all preconditions are met...then - by contract -
the postconditions are met on returning from the function.

What is "debugging mode"?

You aren't actually talking about _manual_ testing of some
kind, are you? If not, I don't understand how you can be
talking about automated testing, yet claiming that unit
tests are redundant. Or are you simply saying that proper
use of DBC can somewhat _reduce_ the number of unit tests
you have to write? (In which case I ask how do you propose
to verify that your precondition contracts are written properly?)

-Peter

 

[aku]

What is "debugging mode"?

You aren't actually talking about _manual_ testing of some
kind, are you?

no I'm not

If not, I don't understand how you can be
talking about automated testing, yet claiming that unit
tests are redundant. Or are you simply saying that proper
use of DBC can somewhat _reduce_ the number of unit tests
you have to write?

yes - the latter. Indeed reduce, not omit. A nr of unittests will
still be necessary to ensure preconditions, but in
the (oversimplified) example I gave (n = 1), the test
"if n < 0: ..." isn't necessary anymore and certainly not *in*
the called function itself.

The "downside" with DBC I see is: when the caller *cannot*
ensure a precondition, then the behavior in the called
function becomes unpredictable.

(In which case I ask how do you propose

 

[Peter Hansen]

A nr of unittests will
still be necessary to ensure preconditions, but in
the (oversimplified) example I gave (n = 1), the test
"if n < 0: ..." isn't necessary anymore and certainly not *in*
the called function itself.

The "downside" with DBC I see is: when the caller *cannot*
ensure a precondition, then the behavior in the called
function becomes unpredictable.

I agree that that appears to be a downside. Furthermore,
if you have to verify in calling code that preconditions
are met, don't you end up with duplication outside of the
function that would otherwise have the check in it?

Well written code will have less duplication, not more,
so I'm still unclear how moving the check out of the
function (from your original example from doctest)
will actually improve things...

And if the code that checks this is in the function,
then a single unit test can verify that the check is
in place and working properly. It sounds like moving
the check out of that function will lead to more
tests and/or more checks in other places, neither of
which is a good idea.

But I'm certainly no expert in (or proponent of) DBC...

-Peter

 

[John Roth]

The "downside" with DBC I see is: when the caller *cannot*
ensure a precondition, then the behavior in the called
function becomes unpredictable.

If the caller cannot insure the precondition, then
they shouldn't be calling that particular function.
The function is not providing the needed service.
This is a design issue, of course. DBC is not a
license to shove all the dirty work onto the caller;
it's a way of clearly separating responsibilities in
a useful fashion.

John Roth

 

[Yermat]

I agree that that appears to be a downside. Furthermore,
if you have to verify in calling code that preconditions
are met, don't you end up with duplication outside of the
function that would otherwise have the check in it?

Well written code will have less duplication, not more,
so I'm still unclear how moving the check out of the
function (from your original example from doctest)
will actually improve things...

And if the code that checks this is in the function,
then a single unit test can verify that the check is
in place and working properly. It sounds like moving
the check out of that function will lead to more
tests and/or more checks in other places, neither of
which is a good idea.

But I'm certainly no expert in (or proponent of) DBC...

-Peter

see http://www.python.org/doc/essays/metaclasses/Eiffel.py
to now how to do (at least one way to) design by contract in Python.

Yermat

 

[Peter Hansen]

see http://www.python.org/doc/essays/metaclasses/Eiffel.py
to now how to do (at least one way to) design by contract in Python.

This doesn't appear to do what the OP says it should do.
I see preconditions which, while coded in separate methods
from the code for which it is written, still executes
every time the method is called. That is, in terms of the
sequence of code, it's the same as just putting the check
in at the top of the called method.

-Peter

 

[Colin Blackburn]

This doesn't appear to do what the OP says it should do.
I see preconditions which, while coded in separate methods
from the code for which it is written, still executes
every time the method is called. That is, in terms of the
sequence of code, it's the same as just putting the check
in at the top of the called method.

In this case yes because python does not support DbC within itself.
However, in a language that does support DbC (Eiffel) these checks can be
turned on during the implementation phase and turned off in the delivered
code. There are techniques in python, java and other languages to
implement DbC using comments and documentation, ie the contract checks are
only executed when a tool/module able to process the structure comments is
loaded.

DbC though is about design rather than just a way testing of parameters.
It is a philosophy of program design. See Object Oriented Software
Construction, ed 2, by Bertrand Mayer.

Colin
--

 

[Peter Hickman]

But in "design by contract" this responsibility is squarely
on the shoulders of the caller, and is *not* checked in
the function.

Are you sure about this. If the called function did the checking then it
will always be checked and the checks would be in one place and easy to
update. If it the checks were done by the caller then the tests need to
be placed everywhere the function is called. That alone would be a
maintenance mightmare.

Looking at the Eiffel site the contract is enforced within the called
function.

put (x: ELEMENT; key: STRING) is
-- Insert x so that it will be retrievable through key.
require
count <= capacity
not key.empty
do
... Some insertion algorithm ...
ensure
has (x)
item (key) = x
count = old count + 1
end

But then this is the python news group so I expect the father of DbC,
Bertrand Meyer, is wrong.

No Smilley

 

[Yermat]

In this case yes because python does not support DbC within itself.
However, in a language that does support DbC (Eiffel) these checks can
be turned on during the implementation phase and turned off in the
delivered code. There are techniques in python, java and other
languages to implement DbC using comments and documentation, ie the
contract checks are only executed when a tool/module able to process
the structure comments is loaded.

DbC though is about design rather than just a way testing of
parameters. It is a philosophy of program design. See Object Oriented
Software Construction, ed 2, by Bertrand Mayer.

Colin
--

Hi,
Not really each time !
As it uses "assert", it is turn off by using -O option of python or by
removing the metaclass ! So it work exactly as DBC implemented in
Eiffel. His author is Bertrand Meyer (with an 'e').
So please re-read it again !

Yermat

 

[Colin Blackburn]

Hi,
Not really each time !
As it uses "assert", it is turn off by using -O option of python or by
removing the metaclass ! So it work exactly as DBC implemented in Eiffel.

It doesn't work exactly as in Eiffel. In Eiffel it is *part* of the
language. Some aspects of DbC can be implemented in other languages but
not all (invariants for instance are not straightforward.)

His author is Bertrand Meyer (with an 'e').
So please re-read it again !

I am so sorry that I typed his name incorrectly. Please don't make me read
all 1000 pages again!!

Colin
--

 

[Colin Blackburn]

Looking at the Eiffel site the contract is enforced within the called
function.

Only while checking is turned on. It is a design philosophy. You specify
the pre and post-conditions before code is even thought of, it is part of
the design.

put (x: ELEMENT; key: STRING) is
-- Insert x so that it will be retrievable through key.
require
count <= capacity
not key.empty
do
... Some insertion algorithm ...
ensure
has (x)
item (key) = x
count = old count + 1
end

This says that *if* the pre-conditions are met (by the caller) *then* the
post-conditions will be guaranteed to be met (by the called method.) All
callers know this because the contract is publicly specified. New callers
can make use of this method because they know what is required of them and
that a given result will be assured if those requirements are met. They
know this because the method has been designed correctly for these
constraints. If the pre-conditions aren't met then not sensible result is
guaranteed.

Colin
--

 

[Peter Hickman]

Only while checking is turned on. It is a design philosophy. You
specify the pre and post-conditions before code is even thought of, it
is part of the design.

Sure but the checks are still made by the function that is called not by
the caller of the function. Which was my point and contrary to what aku
said.

> But in "design by contract" this responsibility is squarely
> on the shoulders of the caller, and is *not* checked in
> the function.


This says that *if* the pre-conditions are met (by the caller) *then*
the post-conditions will be guaranteed to be met (by the called
method.)

No this is not entirely true, the require and ensure and both parts of
the contract. The function will not be called if the require section is
found to be false (such as count being greater than capacity). Then
after the function is executed (the do portion) then second half of the
contract is checked, the ensure section. If these conditions fail then
the contract is broken and the call fail just as if the require had failed.

The require is a contract between the caller and the called. The ensure
is, in effect, a contract between the called and itself. You might get
the require section correct, this would mean that valid parameters have
been passed to the called by the caller. But this is no guarantee that
the do section doesnt screw things up.

Which is why we have the ensure section, this checks that the do section
has not done anything stupid.

Take this as an example (hacked at the keyboard, probably wont work)

double (x: ELEMENT) is
require
x > 0
do
x = x * -2
ensure
x > 0
end

If you call it with double(-12) then the require section fails. If you
call it with double(12) then the require section passes but the do
section is creating a negative number and so the ensure section fails.

Getting the require section to pass is no guarantee that the
post-conditions (ensure section) will be met, the do section is code
like anything else and may get things wrong.

 

[Yermat]

It doesn't work exactly as in Eiffel. In Eiffel it is *part* of the
language. Some aspects of DbC can be implemented in other languages but
not all (invariants for instance are not straightforward.)

It does work exactly the same in effect even if the syntax is not the
same. But we're both right.

I am so sorry that I typed his name incorrectly. Please don't make me
read all 1000 pages again!!

Sometime my fingers are typing without my head. That make things funny. ;-)

 

[Yermat]

It doesn't work exactly as in Eiffel. In Eiffel it is *part* of the
language. Some aspects of DbC can be implemented in other languages but
not all (invariants for instance are not straightforward.)



I am so sorry that I typed his name incorrectly. Please don't make me
read all 1000 pages again!!

Colin
--

I forgot to say that the invariant can be checked each time a function
is called or ended...

Yermat

 

[Colin Blackburn]

Sure but the checks are still made by the function that is called not by
the caller of the function. Which was my point and contrary to what aku
said.

Aku is correct, no checks are (necessarily) made by the function in
installed code. It is the caller's responsibility to satisfy the
pre-conditions.

No this is not entirely true, the require and ensure and both parts of
the contract. The function will not be called if the require section is
found to be false (such as count being greater than capacity).

In the installed code the pre-conditions are not necessarily implemented
therefore the function cannot refuse to run since it does not know its
pre-condition at this stage.

Then after the function is executed (the do portion) then second half of
the contract is checked, the ensure section. If these conditions fail
then the contract is broken and the call fail just as if the require had
failed.

Again, not necessarily in the installed code since the post-conditions are
not known. However, the result will be guaranteed if the preconditions are
met even in the installed code since the code wil have been designed
properly.

Take this as an example (hacked at the keyboard, probably wont work)

double (x: ELEMENT) is
require
x > 0
do
x = x * -2
ensure
x > 0
end

If you call it with double(-12) then the require section fails. If you
call it with double(12) then the require section passes but the do
section is creating a negative number and so the ensure section fails.

Your post-condition is incorrect. The method must ensure that the result
is double the input parameter if that parameter is greater than zero.
Howver, yes in this case the ensure will barf but this is at the design
stage and is there to ensure you get the method right in the first place.
When you deliver this routine the ensure will not be implement but by then
you will have corrected your typo.

Getting the require section to pass is no guarantee that the
post-conditions (ensure section) will be met, the do section is code
like anything else and may get things wrong.

In correctly developed DbC that is precisely what is guaranteed. The
post-condition is *guaranteed* if the pre-condition is met. It is a design
tool.

Colin
--

 

[Daniel Dittmar]

It does work exactly the same in effect even if the syntax is not the
same. But we're both right.

- in Eiffel, postconditions of methods are inherited (because subclasses
must guarantee at least as much). This is difficult to implement with a
simple assert statement.

- postconditions have access to the values parameters and instance variables
had upon entry to the method. This is difficult to support even in a
compiler that knows about these things, at least for mutable objects.

Daniel