[GSOC] regular expressions beta is here

[bearophile]

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