jsverify.js

/*
  copy to jsverify.js
	$ npm install underscore
	$ node jsverify.js

Example output atm:

Property doesn't hold, counterexample with [ 0 ]
inc failing: false
inc fixed: true
Property doesn't hold, counterexample with [ 0, -1 ]
add failing: false
add fixed: true
Property doesn't hold, counterexample with [ 0, -1, 0 ]
add3 failing: false
intersects([1, 2], [1, 3]) true
intersects([1, 2], [3, 4]) false
Property doesn't hold, counterexample with [ [ 4, 4 ], [ -8, -3, -1, 7, -7, -1, -1, -1 ] ]
intersects try 1: false
Property doesn't hold, counterexample with [ [], [] ]
intersects try 2: false
intersects try 3: true

*/
"use strict";

var _ = require("underscore");

var jsc = (function () {
	function assert(exp, message) {
		if (!exp) {
			throw new Error(message);
		}
	}

	function forall(generator, property) {
		assert(typeof property === "function", "property should be a function");

		function test(x) {
			assert(x !== undefined, "generator result should be always not undefined -- temporary self check");

			var r = property(x);
			var r_rec;
			if (r === true) { return true; }
			if (typeof r === "function") {
				r_rec = r(10); // use size
				if (r_rec === true) {
					return true;
				}
			}

			var shrinked = generator.shrink(x);

			for (var i = 0; i < shrinked.length; i++) {
				var y = shrinked[i];

				var rt = test(y);
				if (rt === true) {
					continue;
				} else {
					return rt;
				}
			}

			if (r_rec && r_rec.counterexample) {
				return { counterexample: [x].concat(r_rec.counterexample) };
			} else {
				return { counterexample: [x] };
			}
		}

		return function (size) {
			var x = generator.arbitrary(size); // todo use size
			return test(x);
		};
	}

	function check(property) {
		var size = 5;

		assert(typeof property === "function", "property should be a function");

		for (var i = 0; i < 100; i++) {
			var r = property(size);
			if (r !== true) {
				console.error("Property doesn't hold, counterexample with", r.counterexample);
				return false;
			}
		}

		return true;
	}

	// Random helpers
	/*
	function getRandomArbitrary(min, max) {
		return Math.random() * (max - min) + min;
	}
	*/
	function getRandomInt(min, max) {
		return Math.floor(Math.random() * (max - min + 1) + min);
	}

	// Generators
	function integer(maxsize) {
		maxsize = maxsize || 1000;

		return {
			arbitrary: function (size) {
				size = Math.min(maxsize, size);

				return getRandomInt(-size, size);
			},
			shrink: function (i) {
				i = Math.abs(i);
				if (i === 0) {
					return [];
				} else {
					return [-i+1, i-1];
				}
			},
		};
	}

	function list(generator) {
		generator = generator || integer();

		return {
			arbitrary: function (size) {
				var arrsize = getRandomInt(0, size);
				var arr = new Array(arrsize);
				for (var i = 0; i < arrsize; i++) {
					arr[i] = generator.arbitrary(size);
				}
				return arr;
			},

			shrink: function(arr) {
				function shrink(arr) {
					if (arr.length === 0) {
						return [];
					} else {
						var x = arr[0];
						var xs = arr.slice(1);

						return [xs].concat(
							generator.shrink(x).map(function (xp) { return [xp].concat(xs); }),
							shrink(xs).map(function (xsp) { return [x].concat(xsp); })
						);
					}
				}

				return shrink(arr);
			}
		};
	}

	function nonshrinklist(generator) {
		generator = generator || integer();

		return {
			arbitrary: function (size) {
				var arrsize = getRandomInt(0, size);
				var arr = new Array(arrsize);
				for (var i = 0; i < arrsize; i++) {
					arr[i] = generator.arbitrary(size);
				}
				return arr;
			},

			shrink: function() {
				return [];
			}
		};
	}



	return {
		forall: forall,
		check: check,

		// generators
		integer: integer,
		list: list,
		nonshrinklist: nonshrinklist,
	};
}());

// Failing inc
(function () {
	function inc(i) {
		return i + 1;
	}

	var prop = jsc.forall(jsc.integer(), function (i) {
		return inc(i) === i + 2;
	});

	console.log("inc failing:", jsc.check(prop));
}());

// Working inc
(function () {
	function inc(i) {
		return i + 1;
	}

	var prop = jsc.forall(jsc.integer(), function (i) {
		return inc(i) === i + 1;
	});

	console.log("inc fixed:", jsc.check(prop));
}());

// Failing Add
(function () {
	function add(i, j) {
		return i + (j && 1);
	}

	var prop = jsc.forall(jsc.integer(), function (i) {
		return jsc.forall(jsc.integer(), function (j) {
			return add(i, j) === i + j;
		});
	});

	console.log("add failing:", jsc.check(prop));
}());

// Working Add
(function () {
	function add(i, j) {
		return i + j;
	}

	var prop = jsc.forall(jsc.integer(), function (i) {
		return jsc.forall(jsc.integer(), function (j) {
			return add(i, j) === i + j;
		});
	});

	console.log("add fixed:", jsc.check(prop));
}());

// Failing Add3
(function () {
	function add(i, j, k) {
		return i + (j && 1) + k;
	}

	var prop = jsc.forall(jsc.integer(), function (i) {
		return jsc.forall(jsc.integer(), function (j) {
			return jsc.forall(jsc.integer(), function (k) {
				return add(i, j, k) === i + j + k;
			});
		});
	});

	console.log("add3 failing:", jsc.check(prop));
}());

(function () {
	function contains(arr, x) {
		return arr.indexOf(x) !== -1;
	}

	function intersects(a, b) {
		return a.some(function (x) {
			return contains(b, x);
		});
	}

	console.log("intersects([1, 2], [1, 3])", intersects([1, 2], [1, 3]));
	console.log("intersects([1, 2], [3, 4])", intersects([1, 2], [3, 4]));

	/*
	var prop = jsc.forall(jsc.list(), jsc.list(), function (arr1, arr2) {
		return intersects(arr1, arr2) === (_.intersection(arr1, arr2) !== []);
	});
	*/

	var prop = jsc.forall(jsc.nonshrinklist(), function (a) {
		return jsc.forall(jsc.nonshrinklist(), function (b) {
			return intersects(a, b) === (_.intersection(a, b) !== []);
		});
	});

	console.log("intersects try 1:", jsc.check(prop));

	var prop2 = jsc.forall(jsc.list(), function (a) {
		return jsc.forall(jsc.list(), function (b) {
			return intersects(a, b) === (_.intersection(a, b) !== []);
		});
	});

	console.log("intersects try 2:", jsc.check(prop2));

	var prop3 = jsc.forall(jsc.list(), function (a) {
		return jsc.forall(jsc.list(), function (b) {
			return intersects(a, b) === (_.intersection(a, b).length !== 0);
		});
	});

	console.log("intersects try 3:", jsc.check(prop3));
}());