Kinds of Contracts¶
Crosshair currently recognizes the following kinds of contracts:
The lowest-friction way to get started with CrossHair.
No imports, no new syntax; just use regular Python assert statements.
Compact and doesn’t require a library, but there’s some syntax to learn.
CrossHair can check contracts expressed an a few 3rd party contract libraries.
These contracts use regular Python expressions and are attached to functions with decorators.
Unlike docstring contracts, these contracts can leverage your IDE’s highlighting, refactoring, and autocomplete capabilities.
hypothesis property-based tests can also be checked.
(even though they aren’t “contracts,” strictly speaking)
This is the lowest-investment way to use contracts with CrossHair. You just use regular assert statements in your code. There’s no library to import and no syntax to learn: just use assert statements.
How It Works
CrossHair will analyze any function that starts with one or more assert statements. (it will ignore any function that does not!)
# foo.py from typing import List def remove_smallest(numbers: List[int]) -> None: ''' Removes the smallest number in the given list. ''' # The precondition: CrossHair will assume this to be true: assert len(numbers) > 0 smallest = min(numbers) numbers.remove(smallest) # The postcondition: CrossHair will find examples to make this be false: assert len(numbers) == 0 or min(numbers) > smallest
The leading assert statement(s) are considered to be preconditions: CrossHair will try to find inputs that make these true.
After the precondition asserts, we expect the remaining asserts to pass for all inputs.
The example postcondition above isn’t quite correct: it fails when there are duplicates of the smallest number. CrossHair can tell you this:
$ crosshair check --analysis_kind=asserts foo.py foo.py:14:error:AssertionError: when calling remove_smallest(numbers = [0, -1, -177, -178, -178])
CrossHair will also complain if your function raises an exception. You can silence this by adding a Sphinx-style raises line in your docstring, like this:
def choose(option: int) -> str: """ Does things. :raises IndexError: when option isn't a valid choice """ ...
PEP 316 Contracts¶
PEP 316 is an abandoned PEP for design-by-contract in Python.
PEP316 pairs well with doctest. Doctest is great for illustrative examples and CrossHair can document behavior more holistically. Some kinds of projects may be able to skip unittest/pytest entirely.
How to Write Contracts
See the PEP 316 specification for details. In short:
Place contracts inside the docstrings for functions.
Declare your post-conditions (what you expect to be true of the function’s return value) like this:
post: __return__ > 0
If you like, you can use a single underscore (
_) as a short-hand for
Functions are checked if they have at least one precondition or postcondition in their docstring.
Declare your pre-conditions (what you expect to be true of the function’s inputs) like this:
pre: x < y
Declare that your function mutates arguments with square brackets after the
When doing so, the old values of the arguments are available in a special object called
post[x]: x > __old__.x
Comparison for the purposes of mutation checking is a “deep” comparison.
Use empty square brackets to assert that the function does not mutate any argument. (no brackets means the opposite - the function may mutate any argument)
If your function can validly raise certain exceptions, declare them like this:
raises: IndexError, ZeroDivisionError
Declare class invariants in the class’s docstring like this:
inv: self.foo < self.bar
Class invariants apply additional pre- and post-conditions to each member function.
Note: Unlike contracts on standalone functions, contracts on class methods often encourage/require contracts on the entire class.
This is because you usually need invariants on the class to describe what states are valid, and then every method must be shown to preserve those invariants.
CrossHair supports checking icontract postconditions and invariants.
Things to know
CrossHair will only analyze functions that have at least one precondition or postcondition (
CrossHair will actually invoke the analyzed code with arbitrary arguments - ensure you do not point it at code that uses the disk or network.
CrossHair supports checking deal postconditions.
Things to know
CrossHair will only analyze functions that have at least one condition to check (
To avoid side effects, CrossHair will not check deal contracts with any of the following markers:
syscall. You may want to further restrict CrossHair using
crosshair: offdirectives (see Configuration).
CrossHair does not (currently) support checking deal class invariants.
CrossHair supports checking hypothesis tests;
crosshair watch --analysis_kind=hypothesis .
Things to know
At present, CrossHair performs much worse with hypothesis tests than the other modes. This is because it is symbolically executing the sophisticated logic inside hypothesis that generates your tests’ inputs.
With effort, we can make improvements. Vote with emoji rections in this bug.
You can find examples in the examples/ directory and try it in your browser at crosshair-web.org.