Static typing, contracts and unit tests

By leonardo maffi

V.1.0, 14 December 2012

Keywords: Programming, bugs, Contract Programming, D language, Ada, Static Typing, Unit Tests.

[Go back to the article index]

Simple programming problems like the ones in Reddit/DailyProgrammer have several qualities. While not being its main purpose, DailyProgrammer pages often contain comparisons between different languages. It's interesting to see how even very old programming languages were able to solve the small programming problems shown in DailyProgrammer. Modern languages solve some newish problems, or they offer better and nicer ways to solve problems, they often offer better ways to program "in the large", but it's important to remember the past and some of the history of computer science. Most ideas present in new languages were present in much older languages.

One way to use DailyProgrammer problems is to think of them as coding katas. As Wikipedia explains, "a code kata is an exercise in programming which helps a programmer hone their skills through practice and repetition." If you solve the same problem in various ways, and you compare those versions keeping your mind open, you often find something to learn.

I like several languages, both dynamic languages and strong static typing, and more. In the end there are many different "good enough" ways to solve such little problems, and often for me it's not easy to tell what are the best solutions. Usually the solutions are better along different measuring axis, and there is no single best solution.

One of the reasons of my appreciation for strong static typing is that it helps me avoid some bugs. Here I mean the old-style kind of strong static typing you see in Ada language, instead of the more advanced static typing you see in Haskell. I appreciate some qualities of Haskell, but I think Ada-style typing is sometimes enough to avoid me most bugs. (Types are not just to avoid bugs, Haskell allows a style of type-driven programming that is less commonly done in Ada, but in this article I focus mostly on bugs).

One of the latest problems asks just to create a grid for Minesweeper:

http://www.reddit.com/r/dailyprogrammer/comments/126905/10272012_challenge_108_intermediate_minesweeper/

Given size of the table, like 15x15, and the number of mines, like 20, a solution should generate some kind of table like:

11211..........
1*2*1..1221111.
11211..1**11*1.
.......1221111.
...111.........
...1*211.......
...112*1111....
11...1111*1....
*1......111....
22.....111...11
*1.....1*21..1*
221..1122*21111
1*21.1*1123*1..
13*2.111.1*321.
.2*2.....112*1.

This is one solution I have written using D language:

import std.stdio, std.string, std.random, std.array, std.range;

alias Cell = char;

Cell[][] makeMines(in uint width, in uint height,
                   in uint mineCount)
in {
    assert(width > 0);
    assert(height > 0);
    assert(mineCount > 0);
    assert(mineCount <= width * height);
} out(mat) {
    assert(mat.length == height);
    int nMines = 0;
    foreach (row; mat) {
        assert(row.length == width);
        nMines += count(row, '*');
        assert(row.countchars("*.12345678") == width);
    }
    assert(nMines == mineCount);
} body {
    enum gInit = '0';
    enum mine = '*';

    auto grid = new Cell[][](height, width);
    foreach (row; grid)
        row[] = gInit;

    auto allPositions = iota(width * height)
                        .randomCover(Random(unpredictableSeed));
    foreach (immutable pos; allPositions.take(mineCount)) {
        immutable int x = pos % width;
        immutable int y = pos / width;
        grid[y][x] = mine;
        foreach (sy; -1 .. 2)
            if (y + sy >= 0 && y + sy < height)
                foreach (sx; -1 .. 2)
                    if (x + sx >= 0 && x + sx < width
                        && grid[y + sy][x + sx] != mine)
                        grid[y + sy][x + sx]++; // Next char
    }

    foreach (ref row; grid)
        row = row.replace([gInit], ".");
    return grid;
}

void main() {
    writefln("%-(%s\n%)", makeMines(15, 15, 20));
}

Some comments on this D solution:
- "Cell" is not strongly typed, it's just an alias, like a typedef in C language.
- The makeMines function takes three unsigned values (this means they are >= 0). In D language if you give such function one or more negative int values, they get an automatic silent cast to uint, becoming unsigned values. Most times this is not what you want, and it's a rich source of troubles and bugs.
- makeMines contains some pre-conditions (the "in" part, it's part of D contract programming syntax) that guard at run-time against wrong input arguments.
- The function also contains some post-conditions (the "out" part) that assert that the output matrix has the desired sizes, that it's rectangular (this means all rows have the same desired length), and verifies it contains the desired number of mines. It also verifies that the rows contain nothing else than the admissible chars (9 mines can't be present around an empty space).
- The post-condition of this D solution doesn't verify the numbers around the mines are correct. Generally it's useful to verify that function results are correct, but such tests require some code. Contract testing code too is sometimes buggy, so probably you don't want to write too much long testing code. On the other hand you are often able to use a very different algorithm to verify the results (like a small and very simple brute-force implementation, that is more likely correct), this means the function and the contracts catch each other bugs. I have used this strategy several times.
- Overall this D solution seems to work, and I like it enough, but it verifies many things at run-time, so it's able to "crash" (raise assert Errors) at run-time in many situations, it's not very "strong". I'd really like to write code with stronger static typing, to remove some possible bugs, or to turn some run-time bugs into good compile-time errors.

What follows is an hypothetical signature + contracts of an alternative D-like solution that is typed more strongly. Some of the things shown here are possible in D with appropriate library code, while other things are less easy to do in D:

alias Cell = Subtype!char("*012345678");

Tuple!(Cell[,], SeedType)
makeMines2(in Natural width, in Natural height,
          in Natural mineCount,
          in SeedType seed) pure @safe
in {
    assert(mineCount <= width * height);
} out(mat) {
    assert(mat.length == height);
    assert(mat[0].length == width);
    int nMines = 0;
    foreach (row; mat)
        nMines += count(row, '*');
    assert(nMines == mineCount);
} body {
    ...
} unittest {
    ...
}

Some notes on this hypothetical D-like code:
- It defines the strong type Cell as a subtype of the type of all chars, and it lists (it's not a set, successors and predecessors are defined) the chars of such subset (Ada has built-in syntax support for this, but here I have used hypothetical library code).
- The makeMines2 function arguments are Natural (present in Ada, but in flexible languages you can define it in library code), this means integer numbers greater than zero (up to some maximum value). 'Natural' is a strong type and you can't give this function negative or zero values, it doesn't accept an int or uint.
- The function also takes a seed for the random number generator and it also returns the updated seed (in the second slot of the return 2-tuple). This means that in theory it's possible to use a pseudo-random generator that doesn't change the global state, so I have annotated the function with "pure" as in D. This built-in annotation means the function is not allowed to do several things (like not being allowed to have certain kinds of side effects), and this makes the function more easy to debug, probably more reliable, etc.
- Inside the pre-condition I have to test just that the requested mine number is not too much large.
- In the post-condition I don't have to verify that the output matrix is rectangular because I have used a "Cell[,]", that with C#-like syntax means such a thing (and it also denotes a different data structure in memory, but this is less important because this program is not performance-critical). Instead of using a built-in syntax, in D you are of course free to use a rectangular matrix type defined in library code as "Matrix!(Cell, 2)" or something similar.
- The D annotation @safe means such function is memory-safe.
- In the post-condition I don't test the presence of wrong chars because Cell is a strong subtype, so it's statically impossible for the matrix to contain something else (this assumes the programmer has not used an unsafe cast to force the assignment of chars not allowed in Cell. Currently the @safe annotation does not prevent the programmer to use this, but a silly named hypothetical @verysafe annotation, or probably better an external lint tool, are able to statically verify such things in the source code).
- Inside the function the matrix is initialized with the '0' char. A well designed built-in or library-defined matrix should allow to specify the default contents of the matrix (this is present in CommonLisp and other languages).
- The makeMines2 function doesn't use "++" to unsafely step to the next char of the Cell type, it's meant to use some kind of "next" function, as in Ada. Going past the last '8' causes a run-time error. Using the tools offered by Ada-SPARK language (or even in ATS language, http://www.ats-lang.org ), it's probably possible to prove this error never happens at run-time. But in this case for such not-high-integrity code the chance of that run-time error seems acceptable.

In a language that supports dependent types (as ATS) it's possible to add more invariants on the types of makeMines2, making it even more stronger. But it's not easy to write such code, because you have to write some kind of proof for the compiler that such invariants are statically true. Often this is not easy nor quick to do. For an extreme example in ATS see this list QuickSort implementation that is proven to be terminating and where its return is guaranteed to be a sorted permutation of its input list:

http://www.ats-lang.org/htdocs-old/EXAMPLE/MISC/quicksort_list_dats.html

Ranjit Jhala, Patrick Rondon and Ming Kawaguchi at Microsoft have designed "liquid types", that try to combine usage simplicity of the normal types with some qualities and static safety offered by dependent types. There is an implementation for a F#-like language:

http://research.microsoft.com/apps/video/dl.aspx?id=103638
http://news.ycombinator.com/item?id=3905956

And there is some work done to support even a C-like language:
http://goto.ucsd.edu/csolve/

Are those Ada-style strong typing features just patches on something that is better solved with a simpler functional language as Haskell that maybe avoids most of those problems in the first place? I don't know.

On related topics, this too much short talk by Amanda Laucher and Paul Snively compares types Vs unit-tests:
http://www.infoq.com/presentations/Types-Tests
https://github.com/psnively/types_vs_tests

- Unit-tests verify that one function, method, class of group of functions are correct regarding certain specified input-output pairs. If tests are well written they sample the borders of the input space, looking for probable places where bugs are, like corner cases. Unit-tests are usually simpler to write for pure functions, because the global state becomes less important (some aspect of the global state is always important, because even pure functions have some side-effects, like allocating memory from the heap, or using some run-time). Tools like Haskell QuickCheck (http://en.wikipedia.org/wiki/QuickCheck ) allow the creation of such input-output pairs more automatically, for some kinds of functions.
- Contract programming as the one in Eiffel or D (and partially in C#, but there are partial library implementations for most principal languages) tests the correctness of the function (or class or struct) for all the inputs (and outputs) it will receive at run-time, during debug-time, or even when it's used in unit-tests. The test code in the contracts has to verify all such cases are correct. Compared to unit-tests the contracts are always tested (unless you disable them for performance reasons), and unlike unit-tests this allows you to catch bugs even when you are using your function in real-world situations. One disadvantage compared to unit-tests is that it's not always possible to fully automatically verify the function output to be semantically correct.
- Strong static typing is usually much more limited in catching semantic errors compared to the other two kinds of code constraints. On the other hand it runs and catches bugs at compile-time (sometimes it's possible to use contract programming at compile-time, see Modern Eiffel and C#), and it tests all possible code paths, while both contracts and unit-tests only verify the correctness of the code in its paths used by the given inputs.

Strong static typing is a mathematical proof that some aspects of your code are correct. Contract programming contain algorithmic code that verifies the correctness of the inputs and outputs of your function for all its inputs it actually receives. Unit-tests are even more far from being a proof, as they mostly test single well-chosen input-output examples.

No one of such tools is enough, but using both strong static typing, contract programming with some free asserts (verified at compile-time where possible, and running at run-time in the other cases), and unit-tests, you are able to catch and avoid many bugs.

[Go back to the article index]