Property Testing with JSVerify · Part II
Tags: jsverify, quickcheck, testing, functional
Published: 2019-03-25 02:21:31

---
title: Property Testing with JSVerify · Part II
series: Property Testing with JSVerify
published: true
description: JSVerify API and Documentation In Greater Depth
tags: jsverify, quickcheck, testing, functional
cover_image: https://thepracticaldev.s3.amazonaws.com/i/fl9fkkpd0kjqo71jfz8f.jpg
---

# Part II: JSVerify Docs and Details

In [Part I](https://dev.to/glebec/property-testing-with-jsverify-part-i-3one) 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](http://haskell.org) 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](https://github.com/jsverify/jsverify#readme).

## 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](https://github.com/ramda/ramda/wiki/Type-Signatures). However, JSVerify's style differs somewhat from Ramda, so below is a short introduction to its particular type syntax.

Documentation | Meaning
--------------|--------
`x : y`           | `x` is of type `y` / must be of type `y` / returns type `y`
`myFunc(   )` | A library method with the name `myFunc`
`myFunc(thing: string) : bool` | `myFunc` takes a parameter `thing` which must be a `string`, and returns a `bool`
`a` | any type at all, so long as it consistent with other "`a`"s in the type signature
`a -> [a]` | A (possibly-anonymous) function which takes in a param of any type `a` and returns an array of `a`-type values
`a -> array a` | Same as above
`a -> b` | A function which takes in params of any type `a` and returns values of any type `b` (possibly the same as `a`)
`message: string?` | An **optional** parameter `message` that must be a `string`
`...` | a variadic number of additional arguments or elements
`= true` | a default value for the preceding parameter
`arbLike: {…}` | a parameter `arbLike` which must be an Object
`{ b: bool }` | an object whose `b` property is of type `bool`
`void` | `undefined`

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](https://github.com/jsverify/jsverify#types) 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.

```js
// 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`](https://github.com/jsverify/jsverify#random-functions) instead, which internally use the seed to produce replicable results.

```js
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 `[]`.

```js
// 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:

```js
// 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`

```js
// 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.

```js
// 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`](https://github.com/jsverify/jsverify/issues/295). 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`:

```js
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.

```js
// 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."

```diff
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:

Verification | Behavior
-------------|---------
`true`       | property is considered verified
falsy values | property is considered failed
most truthy values | property is considered failed, with the value appended to the error message
thenable which fulfills | property depends on fulfillment value (see above)
thenable which rejects | property is considered failed, with the reason appended to the error message
function | property verification depends on function return value

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](https://github.com/jsverify/jsverify#properties).

### `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:

```js
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:

```js
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"](https://github.com/jsverify/jsverify#blessing) generators, shrinks, and arbitraries. We will cover the `bless` methods later in [Part III](https://dev.to/glebec/property-testing-with-jsverify-part-iii-5bp0).)

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

```js
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](https://dev.to/glebec/property-testing-with-jsverify-part-iii-5bp0).