I’ve been thinking a lot about minimal QuickCheck properties required for asserting correctness of functions. I was inspired by Daniel Peeble’s proof of List reverse’s core properties and Matthew Brecknells’s minimisation.

I’ve been taking these ideas and playing around with them in Idris. I have proofs that the following functions only need 2 properties to checked:

• List reverse
• Natural number addition

Having the proof, we know that this is all we have to write to test that Haskell’s list reverse is correct:

reverse1 a = reverse [a] == [a]
reverseFlip xs ys = reverse (xs ++ ys) == reverse ys ++ reverse xs

quickCheck $ reverse1 .&&. reverseFlip

Haskell’s QuickCheck is a really great tool for property-based testing. But what if we’re not using Haskell? I’ve been thinking about this a lot, too.

There have been ports to other languages but most do not do a great job. I’ve tried writing property-based tests using Python but the closest I could get was Hypothesis, which is a good start but not near the quality of QuickCheck. JavaScript suffers from the problem.

What if we could use QuickCheck but to execute Python code? Or node.js code? Or shell code?

I started work on CrossCheck to allow testing across these different environments. The library is a small wrapper for creating program strings and then forking them to an external process.

For example, here’s a custom reverse function written in JavaScript:

module.exports = function(xs) {
  return xs.reduce(function(accum, x) {
      return [x].concat(accum);
  }, []);
};

And here’s CrossCheck testing the list reverse properties for that function:

reverse1 :: JsNumber -> CrossProperty
reverse1 =
  comparePrograms "console.log(require('./reverse')([ {0} ]));"
                  "console.log([ {0} ]);"

reverseFlip :: JsList JsNumber -> JsList JsNumber -> CrossProperty
reverseFlip xs ys =
  comparePrograms "console.log(require('./reverse')( {0}.concat( {1} ) ));"
                  "console.log(require('./reverse')( {1} ).concat(require('./reverse')( {0} )));"
                  (Cross2 xs ys)

main :: IO ()
main = do
  crossCheck nodejsCheck reverse1
  crossCheck nodejsCheck reverseFlip

We’ll get familiar output:

+++ OK, passed 100 tests.
+++ OK, passed 100 tests.

If we break one of the properties, we’ll get:

*** Failed! Falsifiable (after 1 test):
JsInt (-6732904699341542)
"[]\n" /= "[ -6732904699341542 ]\n"

You can see a full example on the GitHub project. The main problem with this approach is that forking twice for every iteration makes these tests fairly slow. Let me know if you have an idea on how to improve the forking method.