> Remember, a test (assuming no nondeterminism) is a complete proof of the proposition it states, it's just that it can state only weak propositions, i.e. typically without quantifiers (forall, exists), and certainly without nested quantifiers.
Typical unit tests (what fans of property based testing would call "example based tests") are existentially quantified propositions, e.g. if we squint at the test suite for a 'sort' function, we'll see propositions like "there exists a list l, such that sort(l) is sorted"; "there exists a list l, such that sort(sort(l)) equals sort(l)", "there exists a list l, such that sort(l) is a permutation of l", etc.
To make those executable, their proofs have to be constructive(/intuitionistic); e.g. we can't rely on double-negatives like "if sort(l) were not sorted it would lead to the following contradiction...". In constructive logic, the only way to prove an existential proposition is to construct a particular example and prove that this example satisfies the proposition. In a unit test, the example is our test data, the proposition is our assertion, and the proof comes from executing the test body to verify that the assertion is 'true'.
Thinking about test suites in this way can clarify our thoughts, which can lead us quite easily towards property-based testing and even inductive theorem proving. For example, consider a test like:
def test_sort_ignores_initial_order() {
assert(
sort([3, 1, 2]) == sort([2, 1, 3])
);
}
This is fine, but we can do better. In particular, those literals have been given as-is, without any indication of their relationship (if any), so anyone reading this test (e.g. after breaking it) has to guess where they came from. Not good for a
specification! In this case it's pretty clear, but I've seen many tests in the RealWorld™ which look like `assert(foo(x) == y)` with very complicated literals for `x` and `y`, where it appears the author just copy-pasted the function's output as `y`, and there's no clear relationship between the two (is the `7` in that dictionary the same as this `7` over here, or is that a coincidence? Oh, it was the sum of that `19` with the `-12` from there...).
Let's make this clearer to readers by stating the relationship:
def test_sort_ignores_initial_order() {
let l = [3, 1, 2];
assert(
sort(l) == sort(reverse(l))
);
}
Now this looks more like an existentially-quantified proposition: for
some list, there is
some permutation of it that gets the same output from `sort`. We prove this proposition, using the list `[3, 1, 2]` and the permutation `reverse`.
Such statements are quite weak, but it's quite easy to strengthen them into the universally-quantified propositions that we actually care about, by abstracting-out hard-coded details that don't matter:
def test_sort_ignores_initial_order(l: List[Int]) {
assert(
sort(l) == sort(reverse(l))
);
}
Such abstraction goes beyond simple data values too, e.g. with a little effort we can abstract over the choice of permutation:
def test_sort_ignores_initial_order(l: List[Int], permutation: Word) {
assert(
sort(l) == sort(permute(l, seed=permutation))
);
}
Unfortunately we can't prove universally-quantified statements just by executing their function body, but there are many paths open to us, with different costs/benefits:
- Recover the old existential test, by running it with the examples as arguments. Hypothesis makes this easy with its `@example` decorator.
- Search for counterexamples, to try and prove ourselves wrong. This is property-based testing, AKA property checking, and supported by many test frameworks (Hypothesis, QuickCheck, etc.); there are different approaches to the search problem, some integrate with fuzzers, etc.
- Run a symbolic execution engine to try and prove it correct. This would be dependent on the language, and may require translation to some external formalism; it may also require a lot of manual effort to guide the tooling; and there's no guarantee it would actually work.
- Use a theorem prover to try and prove it correct. Again, this depends on the language and may require translation. First-order logics can be heavily automated, but struggle with some common patterns (e.g. those which require induction). Higher order logics are more expressive, but the tooling is less automated.
There's obviously a spectrum of outcomes, which depends on the effort required. Whilst most wouldn't recoup the cost of an inductive proof; I think property-based testing is very often worth it, and even symbolic execution could be practical in some everyday business situations.