Cheaper contract checking for data structures

bearophile bearophileHUGS at lycos.com
Wed Apr 2 18:56:14 PDT 2014


When you have a data structure, like an array of integers or a 
binary tree, you sometimes want to denote a subset of them that 
satisfy an invariant, as a sorted array of items or an array that 
satisfies the heap invariant. Tagging such invariants in the type 
system is useful, because you can apply different or more 
specialized algorithms (like a binary search instead of a linear 
one). You can also specialize your lazy higher order functions to 
be aware of such invariants, so applying std.algorithm.group() to 
sorted array could return a sorted range.

A problem with enforcing such invariants is that they sometimes 
change the computational complexity of the algorithms. This 
problem was faced in the assumeSorted/SortedRange of Phobos:

>Assumes $(D r) is sorted by predicate $(D pred) and returns the 
>corresponding $(D SortedRange!(pred, R)) having $(D r) as 
>support. To keep the checking costs low, the cost is $(BIGOH 1) 
>in release mode (no checks for sortedness are performed). In 
>debug mode, a few random elements of $(D r) are checked for 
>sortedness. The size of the sample is proportional $(BIGOH 
>log(r.length)). That way, checking has no effect on the 
>complexity of subsequent operations specific to sorted ranges 
>(such as binary search). The probability of an arbitrary 
>unsorted range failing the test is very high (however, an 
>almost-sorted range is likely to pass it). To check for 
>sortedness at cost $(BIGOH n), use $(XREF algorithm,isSorted).<


The constructor of SortedRange:

     this(Range input)
     {
         this._input = input;
         if(!__ctfe)
         debug
         {
             import core.bitop : bsr;
             import std.conv : text;
             import std.random : MinstdRand, uniform;

             // Check the sortedness of the input
             if (this._input.length < 2) return;
             immutable size_t msb = bsr(this._input.length) + 1;
             assert(msb > 0 && msb <= this._input.length);
             immutable step = this._input.length / msb;
             static MinstdRand gen;
             immutable start = uniform(0, step, gen);
             auto st = stride(this._input, step);
             static if (is(typeof(text(st))))
             {
                 assert(isSorted!pred(st), text(st));
             }
             else
             {
                 assert(isSorted!pred(st));
             }
         }
     }


It's good to eventually have some immutable data structures in 
Phobos. From programming a little in Scala I've seen that 
immutable data structures make coding simpler, they make it 
simpler to write code that uses complex data structures. The 
performance is lower, but I am able to write a not-crashing 
program in less time, or at all.
In some cases once the code is working correctly, I am able to 
rewrite it and replace the immutable data structures (like a 
immutable trie) with faster mutable ones.

For such contracts in immutable situations I have read a nice 
paper, "Lazy Contract Checking for Immutable Data Structures", by 
Robert Bruce Findler et al., that proposes a way to tame the 
computational complexity of contract testing:
http://rfrn.org/~shu/papers/ifl07.pdf

Bye,
bearophile


More information about the Digitalmars-d mailing list