jsverify

JSVerify

Property based checking.

Getting Started

Install the module with: npm install jsverify

Synopsis

var jsc = require("jsverify");

// forall (f : bool -> bool) (b : bool), f (f (f b)) = f(b).
var bool_fn_applied_thrice =
	jsc.forall(jsc.fun(jsc.bool()), jsc.bool(), function (f, b) {
		return f(f(f(b))) === f(b);
	});

jsc.check(bool_fn_applied_thrice);
// OK, passed 100 tests

Documentation

Use with jasmine 1.3.x

Check jasmineHelpers.js file.

API

Testing shows the presence, not the absence of bugs.

Edsger W. Dijkstra

To show that propositions hold, we need to construct proofs. There are two extremes: proof by example (unit tests) and formal (machine-checked) proof. Property-based testing is something in between. We formulate propositions, invariants or other properties we believe to hold, but only test it to hold for numerous (random generated) values.

Types and function signatures are written in Coq/Haskell influented style: C# -style List<T> filter(List<T> v, Func<T, bool> predicate) is represented by filter (v : array T) (predicate : T -> bool) : array T in our style.

jsverify can operate with both synchronous and asynchronous-promise properties. Generally every property can be wrapped inside functor, for now in either identity or promise functor, for synchronous and promise properties respectively.

Some type definitions to keep developers sane:

• Functor f => property (size : nat) : f result
• result := true | { counterexample: any }
• Functor f => property_rec := f (result | property)
• generator a := { arbitrary : a, shrink : a -> [a] }

jsc._ - miscellaneous utilities

assert (exp : bool) (message : string) : void

Throw an error with message if exp is falsy.

id (x : any) : any

Identity function.

isEqual (a b : value) : bool

Equality test for value objects. See value generator.

FMap (eq : a -> a -> bool) : FMap a

Finite map, with any object a key.

Short summary of member functions:

• FMap.insert (key : a) (value : any) : void
• FMap.get (key : a) : any
• FMap.contains (key : a) : obool

isPromise p : bool

Optimistic duck-type check for promises. Returns true if p is an object with .then function property.

withPromise (Functor f) (p : f a) (f : a -> b) : f b

This is functor map, fmap, with arguments flipped. Essentially f(p). If p is promise, returns new promise. Using withPromise makes code look very much CPS-style.

getRandomArbitrary (min max : number) : number

Returns random number from [min, max) range.

getRandomInt (min max : int) : int

Returns random int from [min, max] range inclusively.

getRandomInt(2, 3) // either 2 or 3

Properties

forall (gens : generator a ...) (prop : a -> property_rec) : property

Property constructor

check (prop : property) (opts : checkoptions) : promise result + result

Run random checks for given prop. If prop is promise based, result is also wrapped in promise.

Options:

• opts.tests - test count to run, default 100
• opts.size - maximum size of generated values, default 5
• opts.quiet - do not console.log

Primitive generators

integer (maxsize : nat) : generator integer

Integers, ℤ

nat (maxsize : nat) : generator nat

Natural numbers, ℕ (0, 1, 2...)

number (maxsize : number) : generator number

JavaScript numbers, "doubles", ℝ. NaN and Infinity are not included.

bool () : generator bool

Booleans, true or false.

oneof (args : array any) : generator any

Random element of args array.

string () : generator string

Strings

array (gen : generator a) : generator (array a)

value : generator value

JavaScript value: boolean, number, string, array of values or object with value values.

fun (gen : generator a) : generator (b -> a)

Unary functions.

Generator combinators

pair (a : generator A) (b : generator B) : generator (A * B)

If not specified a and b are equal to integer().

suchthat (gen : generator a) (p : a -> bool) : generator {a | p a == true}

Generator of values that satisfy p predicate. It's adviced that p's accept rate is high.

Contributing

In lieu of a formal styleguide, take care to maintain the existing coding style. Add unit tests for any new or changed functionality. Lint and test your code using Grunt.

• You can use grunt jasmine-build to generate _SpecRunner.html to run tests in your browser of choice.
• Use tabs for indentation

Preparing for release

• run grunt literate to regenerate README.md

Release History

• 0.1.1 Use grunt-literate
• 0.1.0 Usable library
• 0.0.2 Documented preview
• 0.0.1 Initial preview

License

Copyright (c) 2013 Oleg Grenrus. Licensed under the BSD3 license.

Related work

JavaScript

• JSCheck
• claire
• gent
• fatcheck
• quickcheck
• qc.js

Others

• Wikipedia - QuickCheck
• Haskell - QuickCheck Introduction
• Erlang - QuviQ
• Erlang - triq
• Scala - ScalaCheck