[GSOC] regular expressions beta is here

[Don]

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?