Agentultra - Property Based Testing With Javascript

If you are reading this I hope you are already familiar with unit testing, integration testing, and all kinds of testing. One kind of testing you may not have heard of is property based testing. Or maybe you have and you just want to see how it can be done in Javascript. The concept was popularized by the Haskell quickcheck library and has spread to almost every language in use today.

Today we’re going to use the, amazing, jsverify library to give you a taste of how this poweful tool can help guide you to writing more reliable code.

Problem

Our stakeholders are worried about storing customer secrets so they’ve tasked us with building a Caesar Cipher library.

(Just roll with me, ok?)

Approach

Because we’re smart developers we’re going to first start by writing some tests. Our first attempt might look something like this:

import {cipher, decipher} from './caesar'

describe('The Caesar Cipher', () => {

    it('should cipher a basic string', () =>
        assert(cipher(2, 'abc') === 'cde')
    )

})

We then go through the motions of adding enough code to make this test pass, then refactoring, adding another test and so on. After going through this enough times we release the code. And then the error reports start coming in.

Another Problem

It turns out that we can’t enumerate all of the possible strings our module will have to deal with. And we want to make sure that every plain-text string we cipher can be reversed by our decipher function given the same shift amount. This is a property of our module that we would like to be guaranteed!

This is where property based testing comes in. Let’s start with an example:

import jsv from 'jsverify'

describe('The Caesar Cipher', () => {

    it('should decipher the cipher text', () =>
        jsv.assertForall(
            jsv.nat,
            jsv.asciinestring,
            (shift, plaintext) =>
                decipher(base, cipher(base, plaintext)) === plaintext
        )
    )

})

Solution

When we run our new test suite on our old implementation we might see something like this:

1) should decypher the cipher text

0 passing (6ms)
1 failing

1) should decypher the cipher text:
   Error: Failed after 1 tests and 4 shrinks. rngState: 8cb92dcef57360a841; Counterexample: 1; "A?";
   at node_modules/jsverify/lib/jsverify.js:360:15
   at Object.map (node_modules/jsverify/lib/functor.js:35:12)
   at checkThrow (node_modules/jsverify/lib/jsverify.js:354:30)
   at Object.assertForall (node_modules/jsverify/lib/jsverify.js:485:10)
   at Context.it (caesar.spec.js:5:8)

This is exactly what we want when we do property based testing. In order to understand what is going on here let’s break down the test we wrote.

jsv.assertForall(jsv.nat, jsv.asciinestring, ...)

What this function does is generate a bunch of arbitrary input to the function we’ve elided from this example. Forall means for all combinations of arbitrary jsv.nat and jsv.asciinestring (a non-empty ascii string). In order for this assertion to hold true the predicate we pass as the final argument has to hold true in every case.

We don’t have the time to wait around to generate every combination of course. So jsverify will simply generate 100 combinations of arbitrary parameters by default. More or less as we ask for it.

The important thing that this tool does for us during development is give us an error like the one we saw above. When it finds a failing test it gives us an example of the input that created the failure. That example is simplified by the tool to give us the minimal example to trigger the failure.

We can take the minimal example and trigger it in our REPL, play with the code, make some changes and inspect the results of further test runs. As you interact with the verifier in this way it guides you, interactively, to the proper implementation that meets your specifications. And you can be quite confident that your properties hold.

Conclusion

If you imagine software specifications on a scale with unit tests being the most informal to proofs being the most formal then property based tests sit somewhere in the middle. This makes it a great, practical tool to have for the more critical parts of your application.

It’s also a fun way to develop programs. It can feel a bit like a game of Cat and Mouse with the verifier providing counter-examples that break your assertions and you trying to shape your implementation so that they fit within them. The feedback helps to guide your implementation to the correct specification. And as you develop your skills with property testing you may find you can start to reason about your programs in a higher-level, abstract way.

If you want to find more tutorials or examples check out these fine articles: