1 | # JSVerify
|
2 |
|
3 | <img src="https://raw.githubusercontent.com/jsverify/jsverify/master/jsverify-300.png" align="right" height="100" />
|
4 |
|
5 | > Property based checking.
|
6 |
|
7 | [![Build Status](https://secure.travis-ci.org/jsverify/jsverify.svg?branch=master)](http://travis-ci.org/jsverify/jsverify)
|
8 | [![NPM version](https://badge.fury.io/js/jsverify.svg)](http://badge.fury.io/js/jsverify)
|
9 | [![Dependency Status](https://david-dm.org/jsverify/jsverify.svg)](https://david-dm.org/jsverify/jsverify)
|
10 | [![devDependency Status](https://david-dm.org/jsverify/jsverify/dev-status.svg)](https://david-dm.org/jsverify/jsverify#info=devDependencies)
|
11 | [![Code Climate](https://img.shields.io/codeclimate/github/jsverify/jsverify.svg)](https://codeclimate.com/github/jsverify/jsverify)
|
12 |
|
13 | ## Getting Started
|
14 |
|
15 | Install the module with: `npm install jsverify`
|
16 |
|
17 | ## Synopsis
|
18 |
|
19 | ```js
|
20 | var jsc = require("jsverify");
|
21 |
|
22 | // forall (f : bool -> bool) (b : bool), f (f (f b)) = f(b).
|
23 | var boolFnAppliedThrice =
|
24 | jsc.forall("bool -> bool", "bool", function (f, b) {
|
25 | return f(f(f(b))) === f(b);
|
26 | });
|
27 |
|
28 | jsc.assert(boolFnAppliedThrice);
|
29 | // OK, passed 100 tests
|
30 | ```
|
31 |
|
32 |
|
33 | ## Documentation
|
34 |
|
35 | ### Usage with [mocha](http://visionmedia.github.io/mocha/)
|
36 |
|
37 | Using jsverify with mocha is easy, just define the properties and use `jsverify.assert`.
|
38 |
|
39 | Starting from version 0.4.3 you can write your specs without any boilerplate:
|
40 |
|
41 | ```js
|
42 | describe("sort", function () {
|
43 | jsc.property("idempotent", "array nat", function (arr) {
|
44 | return _.isEqual(sort(sort(arr)), sort(arr));
|
45 | });
|
46 | });
|
47 | ```
|
48 |
|
49 | You can also provide `--jsverifyRngState state` command line argument, to run tests with particular random generator state.
|
50 |
|
51 | ```
|
52 | $ mocha examples/nat.js
|
53 |
|
54 | 1) natural numbers are less than 90:
|
55 | Error: Failed after 49 tests and 1 shrinks. rngState: 074e9b5f037a8c21d6; Counterexample: 90;
|
56 |
|
57 | $ mocha examples/nat.js --grep 'are less than' --jsverifyRngState 074e9b5f037a8c21d6
|
58 |
|
59 | 1) natural numbers are less than 90:
|
60 | Error: Failed after 1 tests and 1 shrinks. rngState: 074e9b5f037a8c21d6; Counterexample: 90;
|
61 | ```
|
62 |
|
63 | Errorneous case is found with first try.
|
64 |
|
65 | ### Usage with [jasmine](http://pivotal.github.io/jasmine/)
|
66 |
|
67 | Check [jasmineHelpers.js](helpers/jasmineHelpers.js) and [jasmineHelpers2.js](helpers/jasmineHelpers2.js) for jasmine 1.3 and 2.0 respectively.
|
68 |
|
69 | ## API
|
70 |
|
71 | > _Testing shows the presence, not the absence of bugs._
|
72 | >
|
73 | > Edsger W. Dijkstra
|
74 |
|
75 | To show that propositions hold, we need to construct proofs.
|
76 | There are two extremes: proof by example (unit tests) and formal (machine-checked) proof.
|
77 | Property-based testing is somewhere in between.
|
78 | We formulate propositions, invariants or other properties we believe to hold, but
|
79 | only test it to hold for numerous (randomly generated) values.
|
80 |
|
81 | Types and function signatures are written in [Coq](http://coq.inria.fr/)/[Haskell](http://www.haskell.org/haskellwiki/Haskell) influented style:
|
82 | C# -style `List<T> filter(List<T> v, Func<T, bool> predicate)` is represented by
|
83 | `filter (v : array T) (predicate : T -> bool) : array T` in our style.
|
84 |
|
85 | `jsverify` can operate with both synchronous and asynchronous-promise properties.
|
86 | Generally every property can be wrapped inside [functor](http://learnyouahaskell.com/functors-applicative-functors-and-monoids),
|
87 | for now in either identity or promise functor, for synchronous and promise properties respectively.
|
88 |
|
89 |
|
90 | ### Properties
|
91 |
|
92 |
|
93 | - `forall(arbs: arbitrary a ..., userenv: (map arbitrary)?, prop : a -> property): property`
|
94 |
|
95 | Property constructor
|
96 |
|
97 |
|
98 | - `check (prop: property, opts: checkoptions?): result`
|
99 |
|
100 | Run random checks for given `prop`. If `prop` is promise based, result is also wrapped in promise.
|
101 |
|
102 | Options:
|
103 | - `opts.tests` - test count to run, default 100
|
104 | - `opts.size` - maximum size of generated values, default 5
|
105 |
|
106 | - `opts.quiet` - do not `console.log`
|
107 | - `opts.rngState` - state string for the rng
|
108 |
|
109 |
|
110 | - `assert(prop: property, opts: checkoptions?) : void`
|
111 |
|
112 | Same as `check`, but throw exception if property doesn't hold.
|
113 |
|
114 |
|
115 | - `property(name: string, ...)
|
116 |
|
117 | Assuming there is globally defined `it`, the same as:
|
118 |
|
119 | ```js
|
120 | it(name, function () {
|
121 | jsc.assert(jsc.forall(...));
|
122 | }
|
123 | ```
|
124 |
|
125 | You can use `property` to write facts too:
|
126 | ```js
|
127 | jsc.property("+0 === -0", function () {
|
128 | return +0 === -0;
|
129 | });
|
130 | ```
|
131 |
|
132 |
|
133 | - `sampler(arb: arbitrary a, genSize: nat = 10): (sampleSize: nat?) -> a`
|
134 |
|
135 | Create a sampler for a given arbitrary with an optional size. Handy when used in
|
136 | a REPL:
|
137 | ```
|
138 | > jsc = require('jsverify') // or require('./lib/jsverify') w/in the project
|
139 | ...
|
140 | > jsonSampler = jsc.sampler(jsc.json, 4)
|
141 | [Function]
|
142 | > jsonSampler()
|
143 | 0.08467432763427496
|
144 | > jsonSampler()
|
145 | [ [ [] ] ]
|
146 | > jsonSampler()
|
147 | ''
|
148 | > sampledJson(2)
|
149 | [-0.4199344692751765, false]
|
150 | ```
|
151 |
|
152 |
|
153 | ### Types
|
154 |
|
155 | - `generator a` is a function `(size: nat) -> a`.
|
156 | - `show` is a function `a -> string`.
|
157 | - `shrink` is a function `a -> [a]`, returning *smaller* values.
|
158 | - `arbitrary a` is a triple of generator, shrink and show functions.
|
159 | - `{ generator: nat -> a, shrink : a -> array a, show: a -> string }`
|
160 |
|
161 |
|
162 | ### DSL for input parameters
|
163 |
|
164 | There is a small DSL to help with `forall`. For example the two definitions below are equivalent:
|
165 | ```js
|
166 | var bool_fn_applied_thrice = jsc.forall("bool -> bool", "bool", check);
|
167 | var bool_fn_applied_thrice = jsc.forall(jsc.fn(jsc.bool()), jsc.bool(), check);
|
168 | ```
|
169 |
|
170 | The DSL is based on a subset of language recognized by [typify-parser](https://github.com/phadej/typify-parser):
|
171 | - *identifiers* are fetched from the predefined environment.
|
172 | - *applications* are applied as one could expect: `"array bool"` is evaluated to `jsc.array(jsc.bool)`.
|
173 | - *functions* are supported: `"bool -> bool"` is evaluated to `jsc.fn(jsc.bool())`.
|
174 | - *square brackets* are treated as a shorthand for the array type: `"[nat]"` is evaluated to `jsc.array(jsc.nat)`.
|
175 |
|
176 |
|
177 |
|
178 | ### Primitive arbitraries
|
179 |
|
180 |
|
181 | - `integer: arbitrary integer`
|
182 | - `integer(maxsize: nat): arbitrary integer`
|
183 | - `integer(minsize: integer, maxsize: integer): arbitrary integer`
|
184 |
|
185 | Integers, ℤ
|
186 |
|
187 |
|
188 | - `nat: arbitrary nat`
|
189 | - `nat(maxsize: nat): arbitrary nat`
|
190 |
|
191 | Natural numbers, ℕ (0, 1, 2...)
|
192 |
|
193 |
|
194 | - `number: arbitrary number`
|
195 | - `number(maxsize: number): arbitrary number`
|
196 | - `number(min: number, max: number): arbitrary number`
|
197 |
|
198 | JavaScript numbers, "doubles", ℝ. `NaN` and `Infinity` are not included.
|
199 |
|
200 |
|
201 | - `uint8: arbitrary nat`
|
202 | - `uint16: arbitrary nat`
|
203 | - `uint32: arbitrary nat`
|
204 |
|
205 |
|
206 | - `int8: arbitrary integer`
|
207 | - `int16: arbitrary integer`
|
208 | - `int32: arbitrary integer`
|
209 |
|
210 |
|
211 | - `bool: generator bool`
|
212 |
|
213 | Booleans, `true` or `false`.
|
214 |
|
215 |
|
216 | - `datetime: generator datetime`
|
217 |
|
218 | Random datetime
|
219 |
|
220 |
|
221 | - `elements(args: array a): generator a`
|
222 |
|
223 | Random element of `args` array.
|
224 |
|
225 |
|
226 | - `char: generator char`
|
227 |
|
228 | Single character
|
229 |
|
230 |
|
231 | - `asciichar: generator char`
|
232 |
|
233 | Single ascii character (0x20-0x7e inclusive, no DEL)
|
234 |
|
235 |
|
236 | - `string: generator string`
|
237 |
|
238 |
|
239 | - `notEmptyString: arbitrary string`
|
240 |
|
241 | Generates strings which are not empty.
|
242 |
|
243 |
|
244 | - `asciistring: generator string`
|
245 |
|
246 |
|
247 | - `json: generator json`
|
248 |
|
249 | JavaScript Objects: boolean, number, string, array of `json` values or object with `json` values.
|
250 |
|
251 | - `value: generator json`
|
252 |
|
253 |
|
254 | - `falsy: arbitrary *`
|
255 |
|
256 | Generates falsy values: `false`, `null`, `undefined`, `""`, `0`, and `NaN`.
|
257 |
|
258 |
|
259 | - `constant(x: a): arbitrary a`
|
260 |
|
261 | Returns an unshrinkable arbitrary that yields the given object.
|
262 |
|
263 |
|
264 |
|
265 | ### Arbitrary combinators
|
266 |
|
267 |
|
268 | - `nonshrink(arb: arbitrary a): arbitrary a`
|
269 |
|
270 | Non shrinkable version of arbitrary `arb`.
|
271 |
|
272 |
|
273 | - `array(arb: arbitrary a): arbitrary (array a)`
|
274 |
|
275 |
|
276 | - `nearray(arb: arbitrary a): arbitrary (array a)`
|
277 |
|
278 |
|
279 | - `pair(arbA: arbitrary a, arbB : arbitrary b): arbitrary (pair a b)`
|
280 |
|
281 | If not specified `a` and `b` are equal to `value()`.
|
282 |
|
283 |
|
284 | - `map(arb: arbitrary a): arbitrary (map a)`
|
285 |
|
286 | Generates a JavaScript object with properties of type `A`.
|
287 |
|
288 |
|
289 | - `oneof(gs : array (arbitrary a)...) : arbitrary a`
|
290 |
|
291 | Randomly uses one of the given arbitraries.
|
292 |
|
293 |
|
294 | - `record(spec: { key: arbitrary a... }): arbitrary { key: a... }`
|
295 |
|
296 | Generates a javascript object with given record spec.
|
297 |
|
298 |
|
299 |
|
300 | - `fn(gen: generator a): generator (b -> a)`
|
301 | - `fun(gen: generator a): generator (b -> a)`
|
302 | Unary functions.
|
303 |
|
304 |
|
305 |
|
306 | ### Generator functions
|
307 |
|
308 |
|
309 | - `generator.constant(x: a): gen a`
|
310 |
|
311 |
|
312 | - `generator.array(gen: Gen a, size: nat): gen (array a)`
|
313 |
|
314 |
|
315 | - `generator.nearray(gen: Gen a, size: nat): gen (array a)`
|
316 |
|
317 |
|
318 | - `generator.string(size: nat): gen string`
|
319 |
|
320 |
|
321 | - `generator.nestring(size: nat): gen string`
|
322 |
|
323 |
|
324 | - `generator.map(gen: gen a, size: nat): gen (map a)`
|
325 |
|
326 |
|
327 | - `generator.oneof(gen: list (gen a), size: nat): gen a`
|
328 |
|
329 |
|
330 | - `generator.combine(gen: gen a..., f: a... -> b): gen b`
|
331 |
|
332 |
|
333 | - `generator.recursive(genZ: gen a, genS: gen a -> gen a): gen a<
|
334 |
|
335 |
|
336 | - `generator.json: gen json`
|
337 |
|
338 |
|
339 |
|
340 | ### Shrink functions
|
341 |
|
342 |
|
343 | - `shrink.noop(x: a): array a`
|
344 |
|
345 |
|
346 | - `shrink.tuple(shrinks: (a -> array a, b -> array b...), x: (a, b...)): array (a, b...)`
|
347 |
|
348 |
|
349 | - `shrink.array(shrink: a -> array a, x: array a): array (array a)`
|
350 |
|
351 |
|
352 | - `shrink.nearray(shrink: a -> nearray a, x: nearray a): array (nearray a)`
|
353 |
|
354 |
|
355 | - `shrink.record(shrinks: { key: a -> string... }, x: { key: a... }): array { key: a... }`
|
356 |
|
357 |
|
358 |
|
359 | ### Show functions
|
360 |
|
361 |
|
362 | - `show.def(x : a): string`
|
363 |
|
364 |
|
365 | - `show.tuple(shrinks: (a -> string, b -> string...), x: (a, b...)): string`
|
366 |
|
367 |
|
368 | - `show.array(shrink: a -> string, x: array a): string`
|
369 |
|
370 |
|
371 |
|
372 | ### Random functions
|
373 |
|
374 |
|
375 | - `random(min: int, max: int): int`
|
376 |
|
377 | Returns random int from `[min, max]` range inclusively.
|
378 |
|
379 | ```js
|
380 | getRandomInt(2, 3) // either 2 or 3
|
381 | ```
|
382 |
|
383 |
|
384 | - `random.number(min: number, max: number): number`
|
385 |
|
386 | Returns random number from `[min, max)` range.
|
387 |
|
388 |
|
389 |
|
390 | ### Utility functions
|
391 |
|
392 | Utility functions are exposed (and documented) only to make contributions to jsverify easy.
|
393 | The changes here don't follow semver, i.e. ther might backward-incompatible changes even in patch releases.
|
394 |
|
395 | Use [underscore.js](http://underscorejs.org/), [lodash](https://lodash.com/), [ramda](http://ramda.github.io/ramdocs/docs/), [lazy.js](http://danieltao.com/lazy.js/) or some other utility belt.
|
396 |
|
397 |
|
398 | - `utils.isEqual(x: json, y: json): bool`
|
399 |
|
400 | Equality test for `json` objects.
|
401 |
|
402 |
|
403 | - `utils.force(x: a | () -> a) : a`
|
404 |
|
405 | Evaluate `x` as nullary function, if it is one.
|
406 |
|
407 |
|
408 | - `utils.merge(x: obj, y: obj): obj`
|
409 |
|
410 | Merge two objects, a bit like `_.extend({}, x, y)`
|
411 |
|
412 |
|
413 |
|
414 | ## Contributing
|
415 |
|
416 | In lieu of a formal styleguide, take care to maintain the existing coding style.
|
417 |
|
418 | - Add unit tests for any new or changed functionality.
|
419 | - Lint and test your code using `make test`.
|
420 | - Use `make istanbul` to run tests with coverage with [istanbul](http://gotwarlost.github.io/istanbul/).
|
421 | - Create a pull request
|
422 |
|
423 | ### Before release
|
424 |
|
425 | Don't add `README.md` or `jsverify.standalone.js` into pull requests.
|
426 | They will be regenerated before each release.
|
427 |
|
428 | - run `make dist`
|
429 |
|
430 | ## Release History
|
431 |
|
432 | - **0.4.6** — *2014-11-30* better shrinks & recursive
|
433 | - Implemented shrinks: [#51](https://github.com/jsverify/jsverify/issues/51)
|
434 | - `jsc.generator.recursive`: [#37](https://github.com/jsverify/jsverify/issues/37)
|
435 | - array, nearray & map generators return a bit smaller results (*log2* of size)
|
436 | - **0.4.5** — *2014-11-22* stuff
|
437 | - `generator.combine` & `.flatmap`
|
438 | - `nat`, `integer`, `number` & and `string` act as objects too
|
439 | - **0.4.4** — *2014-11-22* new generators
|
440 | - New generators: `nearray`, `nestring`
|
441 | - `generator.constant`
|
442 | - zero-ary `jsc.property` (it ∘ assert)
|
443 | - `jsc.sampler`
|
444 | - **0.4.3** — *2014-11-08* jsc.property
|
445 | - Now you can write your bdd specs without any boilerplate
|
446 | - support for nat-litearls in dsl [#36](https://github.com/jsverify/jsverify/issues/36)
|
447 | ```js
|
448 | describe("Math.abs", function () {
|
449 | jsc.property("result is non-negative", "integer 100", function (x) {
|
450 | return Math.abs(x) >= 0;
|
451 | });
|
452 | });
|
453 | ```
|
454 | - Falsy generator [#42](https://github.com/jsverify/jsverify/issues/42)
|
455 | - **0.4.2** — *2014-11-03* User environments for DSL
|
456 | - User environments for DSL
|
457 | - Generator prototype `map`, and shrink prototype `isomap`
|
458 | - JSON generator works with larger sizes
|
459 | - **0.4.1** Move to own organization in GitHub
|
460 | - **0.4.0** *2014-10-27* typify-dsl & more arbitraries.
|
461 | Changes from **0.3.6**:
|
462 | - DSL for `forall` and `suchthat`
|
463 | - new primitive arbitraries
|
464 | - `oneof` behaves as in QuickCheck (BREAKING CHANGE)
|
465 | - `elements` is new name of old `oneof`
|
466 | - Other smaller stuff under the hood
|
467 | - **0.4.0**-beta.4 generator.oneof
|
468 | - **0.4.0**-beta.3 Expose shrink and show modules
|
469 | - **0.4.0**-beta.2 Move everything around
|
470 | - Better looking README.md!
|
471 | - **0.4.0**-beta.1 Beta!
|
472 | - Dev Dependencies update
|
473 | - **0.4.0**-alpha8 oneof & record -dsl support
|
474 | - also `jsc.compile`
|
475 | - record is shrinkable!
|
476 | - **0.4.0**-alpha7 oneof & record
|
477 | - *oneof* and *record* generator combinators ([@fson](https://github.com/fson))
|
478 | - Fixed uint\* generators
|
479 | - Default test size increased to 10
|
480 | - Numeric generators with size specified are independent of test size ([#20](https://github.com/phadej/jsverify/issues/20))
|
481 | - **0.4.0**-alpha6 more primitives
|
482 | - int8, int16, int32, uint8, uint16, uint32
|
483 | - char, asciichar and asciistring
|
484 | - value → json
|
485 | - use eslint
|
486 | - **0.4.0**-alpha5 move david to be devDependency
|
487 | - **0.4.0**-alpha4 more typify
|
488 | - `suchchat` supports typify dsl
|
489 | - `oneof` → `elements` to be in line with QuickCheck
|
490 | - Added versions of examples using typify dsl
|
491 | - **0.4.0**-alpha3 David, npm-freeze and jscs
|
492 | - **0.4.0**-alpha2 Fix typo in readme
|
493 | - **0.4.0**-alpha1 typify
|
494 | - DSL for `forall`
|
495 | ```js
|
496 | var bool_fn_applied_thrice = jsc.forall("bool -> bool", "bool", check);
|
497 | ```
|
498 |
|
499 | - generator arguments, which are functions are evaluated. One can now write:
|
500 | ```js
|
501 | jsc.forall(jsc.nat, check) // previously had to be jsc.nat()
|
502 | ```
|
503 |
|
504 | - **0.3.6** map generator
|
505 | - **0.3.5** Fix forgotten rngState in console output
|
506 | - **0.3.4** Dependencies update
|
507 | - **0.3.3** Dependencies update
|
508 | - **0.3.2** `fun` → `fn`
|
509 | - **0.3.1** Documentation typo fixes
|
510 | - **0.3.0** Major changes
|
511 | - random generate state handling
|
512 | - `--jsverifyRngState` parameter value used when run on node
|
513 | - karma tests
|
514 | - use make
|
515 | - dependencies update
|
516 | - **0.2.0** Use browserify
|
517 | - **0.1.4** Mocha test suite
|
518 | - major cleanup
|
519 | - **0.1.3** gen.show and exception catching
|
520 | - **0.1.2** Added jsc.assert
|
521 | - **0.1.1** Use grunt-literate
|
522 | - **0.1.0** Usable library
|
523 | - **0.0.2** Documented preview
|
524 | - **0.0.1** Initial preview
|
525 |
|
526 | ## Related work
|
527 |
|
528 | ### JavaScript
|
529 |
|
530 | - [JSCheck](http://www.jscheck.org/)
|
531 | - [claire](https://npmjs.org/package/claire)
|
532 | - [gent](https://npmjs.org/package/gent)
|
533 | - [fatcheck](https://npmjs.org/package/fatcheck)
|
534 | - [quickcheck](https://npmjs.org/package/quickcheck)
|
535 | - [qc.js](https://bitbucket.org/darrint/qc.js/)
|
536 | - [quick\_check](https://www.npmjs.org/package/quick_check)
|
537 | - [gencheck](https://github.com/graue/gentest)
|
538 |
|
539 | ### Others
|
540 |
|
541 | - [Wikipedia - QuickCheck](http://en.wikipedia.org/wiki/QuickCheck)
|
542 | - [Haskell - QuickCheck](http://hackage.haskell.org/package/QuickCheck) [Introduction](http://www.haskell.org/haskellwiki/Introduction_to_QuickCheck1)
|
543 | - [Erlang - QuviQ](http://www.quviq.com/index.html)
|
544 | - [Erlang - triq](https://github.com/krestenkrab/triq)
|
545 | - [Scala - ScalaCheck](https://github.com/rickynils/scalacheck)
|
546 | - [Clojure - test.check](https://github.com/clojure/test.check)
|
547 |
|
548 | The MIT License (MIT)
|
549 |
|
550 | Copyright (c) 2013, 2014 Oleg Grenrus
|
551 |
|
552 | Permission is hereby granted, free of charge, to any person obtaining a copy
|
553 | of this software and associated documentation files (the "Software"), to deal
|
554 | in the Software without restriction, including without limitation the rights
|
555 | to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
556 | copies of the Software, and to permit persons to whom the Software is
|
557 | furnished to do so, subject to the following conditions:
|
558 |
|
559 | The above copyright notice and this permission notice shall be included in
|
560 | all copies or substantial portions of the Software.
|
561 |
|
562 | THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
563 | IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
564 | FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
565 | AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
566 | LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
567 | OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
568 | THE SOFTWARE.
|