A note about ranged types

[bearophile]

This post contains lazy thoughts born from this line:
Ranged numeric types: Ranged!(int, 0, 10)

present in the slide 46 of this document recently shown by Walter:
http://www.slideshare.net/dcacm/patterns-of-human-error

Feel free to ignore this post, because it contains nothing of immediate value.

This little program is just an example (you have to assume that generally the body of this function is longer, it may call other sub-functions, etc). It takes as input an unsigned 'n' and it must return an array of n integers in [0, n) (the actual value of the integers is not specified, so a array of n zero integers is OK).

n is not known at compile-time. The program contains two bugs, the result array is longer than n, and one of its values is larger than n-1:


int[] foo(size_t n)
out(result) {
    assert(result.length == n);
    foreach (x; result)
        assert(x >= 0 && x < n);
} body {
    auto array = new int[n+1]; // bug #1
    array[0] = n+1; // bug #2
    return array;
}

void main(string[] args) {
    foo(args.length);
}


Experience in debugging shows that you want your program to blow up as close (and soon) as possible where the bugs actually are, because this reduces debugging time and makes debugging more easy. The foo() post-condition _is_ able to catch both bugs (the program stops at the first assert. If you fix the first bug it then finds the second), but the bugs are found in the out(){} and not inside the body{} where they are. If the body {} is longer, and it calls other functions, etc, finding the bug may require some time.

This foo() function is silly and useless but it's able to show two of the most common invariants you want in code that uses arrays: enforcing the an array has a specific length (known at run-time) (or a length no bigger than a value), and enforcing some (simple) invariant on the items it contains.

The ranges of Ranged numeric types are compile-time constants. If the bounds are not known at compile-time, then array[] has to know the invariant of its items (when you assign a value to the array, it performs a run-time test to be sure the value is in [0,n). Currently you can't attach an invariant() function to a built-in array, or a pre-condition to its assign method).

A general solution to this class of problems asks for a complex type system (dependent types), but Ada language shows that you are able to catch most array-related bugs even with a much less fancy type system, able to assert only few things/invariants.

Bye,
bearophile