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 a given set 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:
>>> check(prop_sorted_twice)
+++ OK, passed 360 tests: prop_sorted_twice$ python -i leancheck.py
>>> from leancheck import *
>>> def prop_sorted_twice(xs: list[int]) -> bool:
... return sorted(sorted(xs)) == sorted(xs)
...
>>> check(prop_sorted_twice)
+++ OK, passed 360 tests: prop_sorted_twice
>>> def prop_sorted_len(xs: list[int]) -> bool:
... return len(sorted(xs)) == len(xs)
...
>>> check(prop_sorted_len)
+++ OK, passed 360 tests: prop_sorted_len
>>> def prop_sorted_wrong(xs: list[int]) -> bool:
... return sorted(xs) == xs
...
>>> check(prop_sorted_wrong)
*** Failed! Falsifiable after 6 tests:
prop_sorted_wrong([1, 0])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 didn't 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. The (current) idea is mostly to stay as close as I could to the Haskell version. I will note the differences (and similarities) here, once I am done with the LeanCheck prototype and after I take a closer look at Hypothesis. LeanCheck test generation is enumerative, Hypothesis test generation is (likely) random.