Handling Nondeterminism in CrossHair

CrossHair and Such

17 May 2022

CrossHair v0.0.23 was released today with an important new capability for dealing with nondeterministic behavior. Let’s get into it.

Handling Nondeterminism

CrossHair will fail or even yield a incorrect result if you run it on nondeterministic code.

Here are some common things that cause nondeterminism:

As you might imagine, it’s very common to use functions like these. Now, with the work that Loïc Montandon just integrated, we have ways to check properties even when nondeterministic behavior exists.

By identifing the core functions that contain the nondeterminism, we can now tell CrossHair to skip them and instead allow the function to return any value.

One can also apply contracts to these functions to constrain the parameters and return value.

What’s more, this capability is part of the plugin system, so you can create this kind of behavior for 3rd party modules in a reusable & shareable fashion.

You can read more about this capability in the updated plugins docs!

What’s Up Next?

As always, thanks for taking some time to share this journey with me. - Phil