On 08/12/2011 01:31 PM, Don wrote:
bearophile wrote:
Don:
2) I have found many situations where I am able to solve a problem
with both a simple and slow brute force solver, and a complex and
fast algorithm to solve a problem. The little program maybe is too
much slow for normal usage, but it's just few lines long (especially
if I use lot of std.algorithm stuff) but it's much less likely to
contain bugs.
Sorry, but personally I don't believe that this is useful outside of
toy examples.
The question is, what bugs does it find that aren't found by a
trivial unit test?
There are two cases:
(1) it's a very tight test. In which case, it's essentially a unit test.
or (2) it's a very loose test. In which case, it doesn't find bugs.
Putting a simpler algorithm in the post-condition implements a third
possibility you are missing.
Usually unit tests verify some specific cases (you are also able to
add generic testing code in the unit test, but this is just like
moving the postcondition elsewhere).
If you put an alternative algorithm in the postcondition (under
debug{} if you want), you have some advantages:
- It's tight, because the second algorithm is supposed to always give
the same results as the function.
- It works with the real examples the program is run too, not just the
cases you have put in the unit test.
Conditions required for this to be true:
(1) the function must not be time critical;
If the difference is not an asymptotic one, it can well be time critical
(then the debug version will just not be as responsive as would be
desirable for a finished product, which is often the case anyways.)
(2) an alternative algorithm must exist;
If an optimized version exists, a slower one exists too.
(3) the alternative algorithm must be bug-free;
That is often trivial. Also, if it is buggy, the discrepancy will be
caught by the contract and the bug can be fixed.
(4) the function must not have been tested properly;
Usually, large software that has been 'tested properly' still contains
bugs. For mission critical tasks, a form of testing related to this one
is used heavily (multiple teams implement the same specification and the
result of each query to the software is determined by majority vote).
(5) the faulty test cases must occur during debugging (they won't be
caught during production);
Sure. This can catch eg. regressions during development, If there is a
large team of programmers involved, contracts are more useful than if
there is only a single developer.
(6) the programmer must remember to put the asserts in the 'out'
contract, but not put them into the body of the function.
Well, if he they are a seasoned contract programmer, this is not a
problem at all. ;)
This doesn't leave much.
I disagree.
Sometimes you forget to add certain cases in the unittests. Putting the
test in the postcondition makes sure it always run, for all the inputs
your function is run on (unless you disable it), so you will catch the
cases you didn't think of in the unittests.
The crucial feature is, they do NOTHING except find bugs in the function
they are attached to.
They specify what the function is supposed to do, in a way that always
is up to date because it gets checked.
In Eiffel you have the prestate too (the old), so the postcondition is
the only place where such information is usable. I hope prestate will
be added to D DbC, because it's a majob sub-feature of DbC. But I
don't agree that postconditions are useless in D.
??? Does that relate to my sentence in any way?
Yes. He says that once prestate is available, out contracts will be more
useful. But he thinks they are already quite valuable without them.
For starters, it really needs to be a function with multiple return
values. Otherwise, you can just stick asserts just before your return
statement, and you don't need __old or any such thing.
If a function has multiple return values the out(result) helps make
sure all the return paths are verified.
That's what I said.
If the function has only one return value it helps anyway, because it
helps you not forget to verify the result.
???? Why would you remember to put an assert in the postcondition, when
you didn't put it into the function?
Don wrote
> bearophile wrote:
>> If a function has multiple return values the out(result) helps make
>> sure all the return paths are verified.
>
> That's what I said.
Exactly that reason:
int foo(){
// some code
if(condition) return 37; // added after 2h of debugging
// more code
result=...;
assert(condition(result));
return result;
}
int foo()
out(result){assert(condition(result));}
body{
//some code
if(condition) return 37;
// more code
return ...;
}
it is both more convenient (you don't have to change your program logic)
and less error-prone.
Furthermore, all other programmers on the project can immediately check
the postcondition and rely on that it holds for the result of any call
of foo, even if the compiler does not use the out contract for any
theorem proving. They can even do that before the respective function is
implemented correctly. Out contracts are particularly useful when they
are written before the function has is implemented completely.
Under what circumstances are they are more valuable than any other
assert inside a function?
I have already given some answers.
No you haven't.
Another answer is this:
int foo(int x)
in {
// ...
}
out(result) {
auto y = computeSomething(result);
assert(y ...);
assert(y ...);
}
body {
// ...
}
The out{} helps you organize your code, separating the tests of the
body from the postcondition tests. Also in the postcondition you are
allowed to define new variables and call things. All this out(){} code
vanishes in release mode. Ho do you do that with just asserts inside
the body?
If you do this the asserts will vanish in release mode, but the y will
be computed still, wasting computations (a smart compiler is able to
see y is not used and etc, but it's not sure this optimization happens
if the computation of y is complex and it's done in-place):
int foo(int x)
in {
// ...
}
body {
result = ...;
auto y = computeSomething(result);
assert(y ...);
assert(y ...);
return result;
}
I presume there are ways to disable the computation of y in release
mode, but I don't want to think about them. I just stick the y
computation in the postcondition and the compiler will take care of it.
Trivial!
Make the postcondition a nested function. (You can even make it a
delegate literal, if it's only used in one place).
Because everyone who is working on the project wants to check nested
functions? Sure it works, but it is not the best way to implement
contract programming. That is why D has language support that goes
beyond that.
I'll explain my original statement further: If you have a theorem
prover, then the theorem prover can use the 'out' contract in any
function which calls that function.
Eg,
int square(int x) out { assert(result>=0); } body { return x*x; }
void foo()
{
int q = square(-5);
if (q < 0) { .... }
}
Theorem prover knows that q>=0, even if it doesn't have access to the
body of 'square'. So it detects unreachable code in foo().
Theorem prover detects bug in square.
So in this case, the 'out' contract can be used to find bugs in code
that the author of the contract didn't write.
Otherwise, out contracts only find bugs in the local function, which
doesn't have much value, since unit testing already performs that role
(and does it better).
In this case, obviously all the unit tests tested square with an input
that was less than 2^^16 in absolute value. Writing the postcondition
sometimes also allows you to reflect properly on what the precondition
should be. Also, it will be tested on possibly unexpected input.
By contrast, 'in' functions ALWAYS find external bugs rather than local
ones, so they're an order of magnitude more valuable in the current
implementation.
Not always. Sometimes they find bugs in the specification or the in
contract itself.
Contracts are not only an instrument of verification, but also one of
specification.
http://en.wikipedia.org/wiki/Design_by_contract
The out contract is not there to verify some internal consistency
conditions, but to specify what the function should compute, in an exact
way, that is always up to date. The out contract is for programmers too,
not only for compilers.
Contract programming is one of these Software Engineering things. :)
The crucial difference between out contract and an assert at the end of
the function is how they are supposed to be used, not how they will work.
This is reflected by the fact that DMD *.di generation will keep the
contracts around.
-Timon
