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.
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 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 of5
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 integeri
is0
, 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. Shrinkingc
would return[a, b]
; shrinkinga
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
: essentiallyarr => '[' + arr.join(', ') + ']'
- by default, most built-in
show
functions are justJSON.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
(seeY
below) - as the return type for the
prop
parameter offorall
(seeX
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:
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.
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.
Top comments (0)