One List, a Thousand Lists

Part 1 of What a Proof Covers.

Here is the rule this series follows around:

reverse [10, 20, 30] = [30, 20, 10]
reverse [30, 20, 10] = [10, 20, 30]

reverse (reverse xs) = xs

The last line should hold for every finite list, where “equals” means the same contents in the same order. This post checks it the two ways most code is checked. The next one proves it.

Two implementations

Both return a reversed copy and leave the input alone.

static int[] Rev(int[] xs)
{
    var ys = (int[])xs.Clone();
    Array.Reverse(ys);
    return ys;
}

func rev(xs []int) []int {
	ys := append([]int(nil), xs...)
	slices.Reverse(ys)
	return ys
}

An example test

int[] sample = { 10, 20, 30 };

if (!Rev(Rev(sample)).SequenceEqual(sample))
{
    throw new Exception("Reversing twice changed the list.");
}

func TestReverseTwice(t *testing.T) {
	xs := []int{10, 20, 30}
	got := rev(rev(xs))
	if !slices.Equal(got, xs) {
		t.Fatal(got)
	}
}

Both pass. What they establish is that the rule holds for [10, 20, 30]. I chose that list, so the test also inherits whatever I failed to think of: the empty list, one element, repeated values, a list long enough to matter.

A property test

A property test states the rule once and lets a library choose the inputs. In C# I use Hedgehog:

using Hedgehog;
using Hedgehog.Linq;
using Gen = Hedgehog.Linq.Gen;
using Range = Hedgehog.Linq.Range;

var lists = Gen.Int32(
    Range.Constant(-100, 100))
    .List(Range.Constant(0, 100));

var property =
    from xs in lists.ForAll()
    let a = xs.ToArray()
    select Rev(Rev(a))
        .SequenceEqual(a);

property.Check();

In Go, the standard library’s testing/quick is enough:

func TestReverseProperty(t *testing.T) {
	rule := func(xs []int) bool {
		return slices.Equal(
			rev(rev(xs)), xs)
	}
	cfg := &quick.Config{MaxCount: 1000}
	if err := quick.Check(rule, cfg); err != nil {
		t.Fatal(err)
	}
}

Both pass too. This is much better evidence than one list. The empty list and the single element are now among the inputs, and when a property fails, Hedgehog shrinks the failing input to a small one. Go’s testing/quick reports the input it found and does not shrink.

What a passing run means

It is worth saying exactly what was established, because the wording is where the confusion starts.

A passing property test says that no counterexample turned up among the inputs that were generated. The generator decides what “the inputs” means. Mine never produces a list of 101 elements or the value 101. A bug that needs either one is outside the test, and a green run says nothing about it.

For reversing a list this does not matter; no length is special. It matters as soon as the code has a boundary the generator does not reach, such as a length near the largest value an integer can hold. A generator that picks values uniformly from a wide range almost never lands there, which is one reason fuzzers and property tests find different bugs.

So far the rule is checked for one list and for a thousand. The claim was about every list. Closing that gap takes a different kind of argument.

Next: Every List