Part II: JSVerify Docs and Details

In Part I we explored what property checking is, its benefits over traditional unit testing, and saw some of the basics of using the JSVerify library.

JSVerify's official description is "Property-based checking. Like QuickCheck." Since QuickCheck is a Haskell library, JSVerify uses functional jargon and idioms that may be unfamiliar to JavaScript developers. In Part II, we take a close look at the language and concepts of JSVerify's API documentation.

Type Documentation

Functional programming and static types are highly complementary. Type signatures specify sets of allowed inputs and resulting outputs for a given function, which in turn inform the programmer how functions can be used and combined.

In the JSVerify docs, "types and function signatures are written in Coq/Haskell-influenced style". One of the best explanations of Haskell-style type signatures in JS is the Ramda Wiki. However, JSVerify's style differs somewhat from Ramda, so below is a short introduction to its particular type syntax.

Here is an actual line from the documentation, for example:

assert(prop: property, opts: checkoptions?) : void
  ^      ^       ^       ^         ^     ^      ^
  A      B       C       D         E     F      G

A. documenting the `jsc.assert` function
B. first parameter, named `prop`
C. `prop` must be of type `property` (see below)
D. second parameter, named `opts`
E. `opts` must be of type `checkoptions` (see below)
F. `opts` is an optional parameter
G. `jsc.assert` returns `void` (i.e. `undefined`)

Key JSVerify Types

The property and checkoptions types above certainly don't sound like the more familiar string, bool, etc. In typed functional languages, we often invent our own types as needed to be concise yet unambiguous about which functions work with which values.

Vanilla JS doesn't have a first-class notion of custom types. However, JSVerify's docs use custom type names as aliases for the specific values returned from or expected by certain functions. Below are some of the most important examples.

generator a

"a function (size: nat) -> a"

A generator of type a is any function mapping a "size" (natural number, int >= 0) to a pseudorandom value of type a. For example, a function of type generator string might map 0 to the empty string, 1 to a randomly-chosen character, and 2 to a randomly-constructed two-character string.

In reality, the size input can be interpreted differently depending on the generator, and does not have to literally mean length or value. Some examples:

• jsc.generator.array: the length of generated arrays will be up to the logarithm of the size param. This is presumably a performance-related restriction.
• jsc.number.generator: size is the maximum absolute value, e.g. a size of 5 could result in any number between -5 and +5.
• jsc.bool.generator: the size parameter is ignored, and each bool is returned at a probability of 0.5.

// example `generator hydra`
const generatorHydra = (size) => {
    const hydra = { heads: size ** 2 }
    return hydra
}

Deterministic Randomness

A major feature of QuickCheck-like property testing libraries is that they are deterministically pseudorandom. Given a seed string (via the options object for jsc.assert, or the --jsverifyRngState CLI flag), they will reproduce failing test cases exactly, helping the developer to investigate the failure.

When implementing a custom generator, it is important to adhere to this implementation detail, and not use Math.random. JSVerify provides utility functions jsc.random and jsc.random.number instead, which internally use the seed to produce replicable results.

const randomGreetingGenerator = (ignoredSize) => {
    const pseudoRandomIndex = jsc.random(0, 2)
    return ['hi', 'yo', 'sup'][pseudoRandomIndex]
})

shrink a

"a function a -> [a], returning smaller values"

A shrink of type a is a function which given a value of type a returns an array of "smaller" values of type a. "Smaller" is an abstract concept which will vary for each type, but in general will mean fewer elements, numbers closer to zero, etc.

• jsc.shrink.integer: if the input integer i is 0, the shrink returns an empty array []; else, i is mapped to the finite series [0, ⌊1/2·i⌋, -⌊1/2·i⌋, ⌊3/4·i⌋, -⌊3/4·i⌋, …].
• jsc.bool.shrink: in essence, bool => bool ? [false] : []
• jsc.elements.shrink: the elements generator returns randomly-selected values from an array, e.g. [a, b, c]; the elements shrink returns the sub array to the left of whatever element is being shrunk. Shrinking c would return [a, b]; shrinking a returns [].

// example `shrink hydra`
const shrinkHydra = (hydra) => {
    if (hydra.heads <= 0) return []
    // theoretically valid but impractically inefficient:
    return [{ heads: hydra.heads - 1 }]
}

When an input case fails a property check, JSVerify uses the shrink function to search for smaller cases that also fail. If JSVerify finds that an early value in the output array fails, it can skip property-checking and shrinking of the later values. Good shrinks therefore place small, likely-to-fail values near the start of their output:

// example `shrink hydra`
const shrinkHydra = (hydra) => {
    if (hydra.heads <= 0) return []
    // a more practical shrink:
    return [
        { heads: 0 }, // a common & minimal edge case
        { heads: Math.floor(hydra.heads * 1/2) }, // potential time-saver
        { heads: Math.floor(hydra.heads * 3/4) },
        { heads: Math.floor(hydra.heads * 7/8) },
        { heads: hydra.heads - 1 } // thorough search
    ]
}

show

"a function a -> string"

In Haskell, the show function converts any data structure in the Show class to a String. Best practice is for the string to be valid Haskell code, so you could reconstruct the data by copying the string into your program.

For JSVerify, show will be called whenever a failing case is reported, with the resulting string included in the error message as the counterexample.

• jsc.show.array: essentially arr => '[' + arr.join(', ') + ']'
• by default, most built-in show functions are just JSON.stringify

// example `show : hydra -> string`
const showHydra = (hydra) => `{ heads: ${hydra.heads} }`

Because failing cases can be replicated using the reported PRNG seed, it is not strictly necessary for show to return valid JS code, but it is often good practice for the same reasons as in Haskell.

arbitrary a

"a triple of generator, shrink and show functions."
{generator: nat -> a, shrink: a -> array a, show: a -> string}

An arbitrary value of type a is a concept tying together the generator, shrink and show functions for a type a. It is implemented in JSVerify via an object wrapping those three functions. For example, the abitrary string type is any object which can generate, shrink, and show strings on demand.

// example `arbitrary hydra`
const arbitraryHydra = {
    generator: generatorHydra,
    shrink: shrinkHydra,
    show: showHydra
}

In some contexts, the shrink and show functions are actually optional. Without a shrink, however, JSVerify will be unable to simplify failing cases; they will be reported as they are.

property

As of this writing, property is used in at least three distinct ways in the JSVerify docs:

• to refer to the library method jsc.property
• as the overall return type for jsc.forall (see Y below)
• as the return type for the prop parameter of forall (see X below)

forall(
    arbs: arbitrary a ...,
    userenv: (map arbitrary)?,
    prop : a -> property       // X
): property                    // Y

Unfortunately, X and Y do not actually refer to the same type, so in my humble opinion the X type should be renamed verification. In the remainder of this article, a property type will refer to Y.

So what is this property type anyway? In short, forall acts as a "property constructor", and other methods like assert and check act as "property consumers". In terms of official JS types, the values returned by forall are of type function:

const prop_strSliceEql = jsc.forall('string', str => str.slice() === str)
console.log(typeof prop_strSliceEql === 'function') // true

However, it is not the role of the developer to manually invoke a property. Rather, property values will be passed to check or assert to actually use them.

// assert(prop: property, opts: checkoptions?) : void
jsc.assert(prop_strSliceEql) // runs without error

Being able to navigate type-based documentation, noting which function outputs and inputs line up, is a key skill in the typed functional programming world. It isn't actually necessary for us to know how property-type values are implemented, because they are an intermediate value both produced by and consumed by JSVerify library methods.

forall( ... ) → property
                   ↓
         assert(property, ...) → void

Verification (unofficial)

As mentioned above, the property returned from prop and the property returned from forall are not the same type, so for our purposes we will (informally) refer to the former as "verifications."

forall(
    arbs: arbitrary a ...,
    userenv: (map arbitrary)?,
-   prop : a -> property
+   prop : a -> verification
): property

Verification values can be any type at all, but JSVerify exhibits different behaviors depending on the type:

Some of the above behaviors are not explicitly documented, and may act in unspecified or unintended ways depending on usage. Caveat emptor.

checkoptions

The options object optionally object passed to check or assert, used to configure number of tests run, the size parameter for generators, an rng seed, etc. Documented here.

env / typeEnv / map arbitrary

An optional argument to the following library methods:

• forall
• compile
• assertForall
• checkForall
• record
• suchthat

The env type is an object which maps names of arbitraries (as string keys) to definitions for arbitraries (as objects). For example:

const arbitraryHydra = {
    generator: generatorHydra,
    shrink: shrinkHydra,
    show: showHydra
}

// : env
const env = {
    hydra: arbitraryHydra
}

Environment objects extend JSVerify's built-in DSL of arbitrary data (e.g. strings, numbers, arrays of arbitraries) with new, custom arbitraries. When you pass in an environment to forall, it is merged with the defaults, so you can specify any mix of data from both sets:

const exampleProp = jsc.forall(
    'nat',             // asking for built-in `arbitrary natural`
    'hydra',           // asking for custom `arbitrary hydra`
    env,               // object providing the `hydra` arbitrary
    (nat, hydra) => {  // property verifier receiving both data
        return hydra.heads + nat > 0
    }
)

(Note that the above example will not yet work, because we have not covered JSVerify's concept of "blessing" generators, shrinks, and arbitraries. We will cover the bless methods later in Part III.)

On the other hand, instead of using the string DSL, you can pass custom arbitraries to forall directly:

const exampleProp = jsc.forall(
    'nat',             // asking for built-in `arbitrary natural`
    arbitraryHydra,    // asking for custom `arbitrary hydra`
    (nat, hydra) => {  // property verifier receiving both data
        return hydra.heads + nat > 0
    }
)

We will see more about using the DSL vs. JS values in Part III.