LeanCheck for Python

This is a port of Haskell's LeanCheck to Python.

LeanCheck is an enumerative property-based testing library. It can be used to complement your unit tests.

This is a work in progress: this library is currently experimental..

The usual drill in unit testing involves making assertions about specific input-output cases of functions, such as:

assertEqual(sorted([4,2,1,3]), [1,2,3,4])

There are no arguments to the unit test.

In property-based testing (with LeanCheck) one writes more general properties that should be true for any assignment of arguments.

For example: given any list, sorting it twice is the same as sorting it once. We can encode this as a function returning a boolean value:

def prop_sorted_twice(xs: list[int]) -> bool:
    return sorted(sorted(xs)) == sorted(xs)

For whatever list we provide this function, it should return True. Now one can use LeanCheck to verify this automatically:

>>> from leancheck import *

>>> check(prop_sorted_twice)
+++ OK, passed 360 tests: prop_sorted_twice

When the property or function-under-test is incorrect LeanCheck may find and report a counterexample like so:

*** Failed! Falsifiable after 6 tests:
    prop_sorted_wrong([1, 0])

This would indicate that the list [1, 0] is an ill input.

Besides using check() to test individual properties, one can use leancheck.main() to test all properties defined in the current file.

Example, testing a sorting function

Consider the following (not-quite) qsort function:

def qsort(lst):
    if lst == []:
        return []
    x, *etc = lst  # split into head and tail
    lesser  = [y for y in etc if y < x]
    greater = [y for y in etc if y > x]
    return qsort(lesser) + [x] + qsort(greater)

It returns the sorted version of the given argument list:

>>> qsort([4,2,1,3])
[1,2,3,4]

We can define the following three properties about it:

1. Sorting a list returns the elements in order;
2. Sorting preserves membership in the list;
3. Sorting does not change the list length.

We can define and test these properties with LeanCheck as follows:

import leancheck

def prop_sort_ordered(xs: list[int]) -> bool:
    ys = qsort(xs)
    return all(x <= y for x, y in zip(ys, ys[1:]))

def prop_sort_elem(x: int, xs: list[int]) -> bool:
    return (x in qsort(xs)) == (x in xs)

def prop_sort_len(xs: list[int]) -> bool:
    return len(qsort(xs)) == len(xs)

if __name__ == '__main__':
    leancheck.main()

We import LeanCheck, define the properties and call leancheck.main() which will test all properties defined in the file: anything named prop_*. The properties may be placed together with the function(s) under test or in a separate test file depending on your needs.

Note the type annotations, these are necessary for LeanCheck to know how to test each property.

Running the above file/program/script yields the following report:

+++ OK, passed 360 tests: prop_sort_ordered

+++ OK, passed 360 tests: prop_sort_elem

*** Failed! Falsifiable after 3 tests:
    prop_sort_len([0, 0])

We actually have a failure in the third property and we can investigate:

>>> leancheck.check(prop_sort_len)
*** Failed! Falsifiable after 3 tests:
    prop_sort_len([0, 0])

>>> prop_sort_len([0, 0])
False

>>> len(qsort([0, 0]))
1

>>> qsort([0, 0])
[0]

Our function discards repeated elements! Fixing the bug in qsort is left as an exercise to the reader.

An extended version of this example can be found under the examples/ folder in the source repository.

Example, custom class

LeanCheck also works for tesing properties over instances of custom classes. The following short example illustrates how to do this:

import leancheck
from leancheck import Enumerator

class Point:
    def __init__(self, x: float, y: float):
        self.x = x
        self.y = y

    def __repr__(self):
        return f"Point({self.x}, {self.y})"

    def distance(self, other):
        return (self.x - other.x)**2 + (self.y - other.y)**2

def prop_distance_positive(p: Point, q: Point) -> bool:
    return Point.distance(p,q) >= 0

def prop_self_distance(p: Point) -> bool:
    return Point.distance(p,p) == 0

leancheck.main(verbose=True)

The enumeration for Points is inferred from the type annotations in the constructor. A point is a cross-product of two floats:

>>> print(Enumerator(Point))
[Point(0.0, 0.0), Point(0.0, 1.0), Point(1.0, 0.0), Point(0.0, -1.0), Point(1.0, 1.0), Point(-1.0, 0.0), ...]

If the type-annotation was not present, an enumerator could be registered for use with:

Enumerator.register_cons(Point, float, float)

... anywhere between the Point class declaration and the leancheck.main call.

Further reading

LeanCheck for Haskell is subject to a chapter in a PhD Thesis (2017).

As of 2024, Python already has a relatively popular property-based testing library called Hypothesis. While writing this port of LeanCheck, I intentionally did not take a closer look at Hypothesis. I want to see if I would take an entirely different approach here by not getting biased of how things were implemented there. ... and indeed I did. Python's LeanCheck stays as close as possible to its Haskell counterpart, here are key differences between LeanCheck and Hypothesis:

	LeanCheck	Hypothesis
test generation	enumerative	random
generator selection	type annotation	strategy decorators
testing individual properties	check() function	properties themselves
testing all properties in file	leancheck.main()	not supported?
development status	experimental	production/stable

LeanCheck is enumerative. The test generators are selected based on type annotations in the properties. One can test an individual property with the check() function. To test all properties in a single test file one can use leancheck.main(). Any function named prop_* with a return type of bool is considered a property by convention. LeanCheck is simpler to use IMHO.