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.
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.
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.
Bye,
bearophile
