bearophile wrote:
Don:
"out" contracts seem to be almost useless, unless you have a theorem prover. The
reason is, that they test nothing apart from the function they are attached to, and it's
much better to do that with unittesting.<
I see three different situations where postconditions are useful in D:
1) Sometimes the result of your function/method must satisfy some simple
condition to be correct.
As example, it must be a nonnegative number. Then you add assert(result >= 0, "..."); in the
out. For a Phobos example, std.algorithm.countUntil postcondition is allowed to test assert(result >=
-1, "...");
Other possible conditions are the output string can't be longer than a certain
amount (like longer than the input string), and so on.
In certain cases the program the finds the solution is slow, but testing the correctness of a function is fast. I have hit many situations like this.
As an example you test if the result of a complex sorting algorithm is ordered, and with the same length of the input (but maybe you don't test for the output items to be the same of the input).
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?
You can't always verify the result of the fast algorithm with the slow
algorithm, this is not useful.
In such situations I write the postcondition like this:
in {
// ...
}
out(result) {
// some fast postconditon tests here
debug {
assert(result == slowAlgorithm(input));
}
body {
// fast algorithm here
}
This way, in release mode it tests nothing, in nonrelease build it tests the
fast postconditions, and in debug mode it also verifies the fast algorithm
gives the same results as the slow algorithm. Generally solving a problem in
two quite different ways helps catch problems in the algorithms.
3) When D will get the prestate ("old" in some contract programming
implementations), I will be able to use the prestate inside the postcondition to verify
better than the function/method has changed the globals, or instance attributes in a
correct way. You can't put such tests in the class/struct invariant, or in the
precondition.
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.
I'm using postconditions often in my code (less often than preconditions, but
often enough). A theorem prover is not strictly necessary for them to be useful.
I would like to see an example of a good postcondition.
The crucial feature is, they do NOTHING except find bugs in the function
they are attached to. So it's very difficult to invent a plausible one.
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.
Under what circumstances are they are more valuable than any other
assert inside a function?
