-
Notifications
You must be signed in to change notification settings - Fork 168
/
proper.erl
2587 lines (2399 loc) · 104 KB
/
proper.erl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%%% -*- coding: utf-8; erlang-indent-level: 2 -*-
%%% -------------------------------------------------------------------
%%% Copyright 2010-2022 Manolis Papadakis <manopapad@gmail.com>,
%%% Eirini Arvaniti <eirinibob@gmail.com>,
%%% Kostis Sagonas <kostis@cs.ntua.gr>,
%%% and Andreas Löscher <andreas@loscher.net>
%%%
%%% This file is part of PropEr.
%%%
%%% PropEr is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU General Public License as published by
%%% the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% PropEr is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
%%% GNU General Public License for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with PropEr. If not, see <http://www.gnu.org/licenses/>.
%%% @copyright 2010-2022 Manolis Papadakis, Eirini Arvaniti, Kostis Sagonas and Andreas Löscher
%%% @version {@version}
%%% @author Manolis Papadakis
%%% @doc This is the main PropEr module.
%%%
%%% == How to write properties ==
%%% The simplest properties that PropEr can test consist of a single boolean
%%% expression (or a statement block that returns a boolean), which is expected
%%% to evaluate to `true'. Thus, the test `true' always succeeds, while the test
%%% `false' always fails (the failure of a property may also be signified by
%%% throwing an exception, error or exit. More complex (and useful) properties
%%% can be written by wrapping such a boolean expression with one or more of the
%%% following wrappers:
%%%
%%% <dl>
%%% <dt>`?FORALL(<Xs>, <Xs_type>, <Prop>)'</dt>
%%% <dd>The `<Xs>' field can either be a single variable, a tuple of variables
%%% or a list of variables. The `<Xs_type>' field must then be a single type,
%%% a tuple of types of the same length as the tuple of variables or a list
%%% of types of the same length as the list of variables, respectively.
%%% Tuples and lists can be combined in any way, as long as `<Xs>' and
%%% `<Xs_type>' are compatible. Both PropEr-provided types, as listed in the
%%% {@link proper_types} module, and types declared in Erlang's built-in
%%% typesystem (we will refer to such types in as <em>native types</em>) may
%%% be used in the `<Xs_type>' field. The use of native types in `?FORALL's is
%%% subject to some limitations, as described in the documentation for the
%%% {@link proper_typeserver} module. All the variables inside `<Xs>' can
%%% (and should) be present as free variables inside the wrapped property
%%% `<Prop>'. When a `?FORALL' wrapper is encountered, a random instance of
%%% `<Xs_type>' is produced and each variable in `<Xs>' is replaced inside
%%% `<Prop>' by its corresponding instance.</dd>
%%% <dt>`?FORALL_TARGETED(<Xs>, <Xs_type>, <Prop>)'</dt>
%%% <dd>This is the targeted version of the `?FORALL' macro that uses the
%%% targeted PBT component of PropEr.</dd>
%%% <dt>`?IMPLIES(<Precondition>, <Prop>)'</dt>
%%% <dd>This wrapper only makes sense when in the scope of at least one
%%% `?FORALL'. The `<Precondition>' field must be a boolean expression or a
%%% statement block that returns a boolean. If the precondition evaluates to
%%% `false' for the variable instances produced in the enclosing `?FORALL'
%%% wrappers, the test case is rejected (it doesn't count as a failing test
%%% case), and PropEr starts over with a new random test case. Also, in
%%% verbose mode, an `x' is printed on screen.</dd>
%%% <dt>`?WHENFAIL(<Action>, <Prop>)'</dt>
%%% <dd>The `<Action>' field should contain an expression or statement block
%%% that produces some side-effect (e.g. prints something to the screen).
%%% In case this test fails, `<Action>' will be executed. Note that the output
%%% of such actions is not affected by the verbosity setting of the main
%%% application.</dd>
%%% <dt>`?EXISTS(<Xs>, <Xs_type>, <Prop>)'</dt>
%%% <dd> The `?EXISTS' macro uses the targeted PBT component of PropEr to try
%%% to find one instance of `<Xs>' that makes the `<Prop>' true. If such a `<Xs>'
%%% is found the property passes. Note that there is no counterexample if no
%%% such `<Xs>' could be found.</dd>
%%% <dt>`?NOT_EXISTS(<Xs>, <Xs_type>, <Prop>)'</dt>
%%% <dd> The `?NOT_EXISTS' macro is similar to the `?EXISTS' macro with the
%%% difference that if an `<Xs>' is found that makes `<Prop>' true, the
%%% property fails and this `<Xs>' is a counterexample to the property.</dd>
%%% <dt>`?TRAPEXIT(<Prop>)'</dt>
%%% <dd>If the code inside `<Prop>' spawns and links to a process that dies
%%% abnormally, PropEr will catch the exit signal and treat it as a test
%%% failure, instead of crashing. `?TRAPEXIT' cannot contain any more
%%% wrappers.</dd>
%%% <dt>`?TIMEOUT(<Time_limit>, <Prop>)'</dt>
%%% <dd>Signifies that `<Prop>' should be considered failing if it takes more
%%% than `<Time_limit>' milliseconds to return. The purpose of this wrapper is
%%% to test code that may hang if something goes wrong. `?TIMEOUT' cannot
%%% contain any more wrappers.</dd>
%%% <dt>`?SETUP(<Setup_fun>, <Prop>)'</dt>
%%% <dd>Adds a setup `<Setup_fun>'ction to the property which will be called
%%% before the first test. This function has to return a finalize function of
%%% arity 0, which should return the atom `ok', that will be called after
%%% the last test.
%%% It is possible to use multiple `?SETUP' macros on the same property.</dd>
%%% <dt>`conjunction(<SubProps>)'</dt>
%%% <dd>See the documentation for {@link conjunction/1}.</dd>
%%% <dt>`equals(<A>, <B>)'</dt>
%%% <dd>See the documentation for {@link equals/2}.</dd>
%%% </dl>
%%%
%%% There are also multiple wrappers that can be used to collect statistics on
%%% the distribution of test data:
%%%
%%% <ul>
%%% <li>{@link collect/2}</li>
%%% <li>{@link collect/3}</li>
%%% <li>{@link aggregate/2}</li>
%%% <li>{@link aggregate/3}</li>
%%% <li>{@link classify/3}</li>
%%% <li>{@link measure/3}</li>
%%% </ul>
%%%
%%% <span id="external-wrappers"></span>
%%% A property may also be wrapped with one or more of the following outer-level
%%% wrappers, which control the behaviour of the testing subsystem. If an
%%% outer-level wrapper appears more than once in a property, the innermost
%%% instance takes precedence.
%%%
%%% <ul>
%%% <li>{@link numtests/2}</li>
%%% <li>{@link fails/2}</li>
%%% <li>{@link on_output/2}</li>
%%% </ul>
%%%
%%% For some actual usage examples, see the code in the examples directory, or
%%% check out PropEr's site. The testing modules in the tests directory may also
%%% be of interest.
%%%
%%% == Program behaviour ==
%%% When running in verbose mode (this is the default), each successful test
%%% prints a '.' on screen. If a test fails, a '!' is printed, along with the
%%% failing test case (the instances of the types in every `?FORALL') and the
%%% cause of the failure, if it was not simply the falsification of the
%%% property.
%%% Then, unless the test was expected to fail, PropEr attempts to produce a
%%% minimal test case that fails the property in the same way. This process is
%%% called <em>shrinking</em>. During shrinking, a '.' is printed for each
%%% successful simplification of the failing test case. When PropEr reaches its
%%% shrinking limit or realizes that the instance cannot be shrunk further while
%%% still failing the test, it prints the minimal failing test case and failure
%%% reason and exits.
%%%
%%% The return value of PropEr can be one of the following:
%%%
%%% <ul>
%%% <li>`true': The property held for all valid produced inputs.</li>
%%% <li>`false': The property failed for some input.</li>
%%% <li>`{error, <Type_of_error>}': An error occurred; see the {@section Errors}
%%% section for more information.</li>
%%% </ul>
%%%
%%% To test all properties exported from a module (a property is a 0-arity
%%% function whose name begins with `prop_'), you can use {@link module/1} or
%%% {@link module/2}. This returns a list of all failing properties, represented
%%% by MFAs. Testing progress is also printed on screen (unless quiet mode is
%%% active). The provided options are passed on to each property, except for
%%% `long_result', which controls the return value format of the `module'
%%% function itself.
%%%
%%% == Counterexamples ==
%%% A counterexample for a property is represented as a list of terms; each such
%%% term corresponds to the type in a `?FORALL'. The instances are provided in
%%% the same order as the `?FORALL' wrappers in the property, i.e. the instance
%%% at the head of the list corresponds to the outermost `?FORALL' etc.
%%% Instances generated inside a failing sub-property of a conjunction are
%%% marked with the sub-property's tag.
%%%
%%% The last (simplest) counterexample produced by PropEr during a (failing) run
%%% can be retrieved after testing has finished, by running
%%% {@link counterexample/0}. When testing a whole module, run
%%% {@link counterexamples/0} to get a counterexample for each failing property,
%%% as a list of `{mfa(), '{@type counterexample()}`}' tuples. To enable this
%%% functionality, some information has to remain in the process dictionary
%%% even after PropEr has returned. If, for some reason, you want to completely
%%% clean up the process dictionary of PropEr-produced entries, run
%%% {@link clean_garbage/0}.
%%%
%%% Counterexamples can also be retrieved by running PropEr in long-result mode,
%%% where counterexamples are returned as part of the return value.
%%% Specifically, when testing a single property under long-result mode
%%% (activated by supplying the option `long_result', or by calling
%%% {@link counterexample/1} or {@link counterexample/2} instead of
%%% {@link quickcheck/1} and {@link quickcheck/2} respectively), PropEr will
%%% return a counterexample in case of failure (instead of simply returning
%%% `false'). When testing a whole module under long-result mode (activated by
%%% supplying the option `long_result' to {@link module/2}), PropEr will return
%%% a list of `{mfa(), '{@type counterexample()}`}' tuples, one for each failing
%%% property.
%%%
%%% You can re-check a specific counterexample against the property that it
%%% previously falsified by running {@link check/2} or {@link check/3}. This
%%% will return one of the following (both in short- and long-result mode):
%%%
%%% <ul>
%%% <li>`true': The property now holds for this test case.</li>
%%% <li>`false': The test case still fails (although not necessarily for the
%%% same reason as before).</li>
%%% <li>`{error, <Type_of_error>}': An error occurred - see the {@section Errors}
%%% section for more information.</li>
%%% </ul>
%%%
%%% Proper will not attempt to shrink the input in case it still fails the
%%% property. Unless silent mode is active, PropEr will also print a message on
%%% screen, describing the result of the re-checking. Note that PropEr can do
%%% very little to verify that the counterexample actually corresponds to the
%%% property that it is tested against.
%%%
%%% == Options ==
%%% Options can be provided as an extra argument to most testing functions (such
%%% as {@link quickcheck/1}). A single option can be written stand-alone, or
%%% multiple options can be provided in a list. When two settings conflict, the
%%% one that comes first in the list takes precedence. Settings given inside
%%% external wrappers to a property (see the {@section How to write properties}
%%% section) override any conflicting settings provided as options.
%%%
%%% The available options are:
%%%
%%% <dl>
%%% <dt>`quiet'</dt>
%%% <dd>Enables quiet mode - no output is printed on screen while PropEr is
%%% running.</dd>
%%% <dt>`verbose'</dt>
%%% <dd>Enables verbose mode - this is the default mode of operation.</dd>
%%% <dt>`{to_file, <IO_device>}'</dt>
%%% <dd>Redirects all of PropEr's output to `<IO_device>', which should be an
%%% IO device associated with a file opened for writing.</dd>
%%% <dt>`{on_output, <Output_function>}'</dt>
%%% <dd>This option disables colored output (i.e,, it implies 'nocolors'), and
%%% makes PropEr use the supplied function for all output printing. This
%%% function should accept two arguments in the style of `io:format/2'
%%% (i.e., a string and a list of arguments) which are supplied to the
%%% function by PropEr.<br/>
%%% CAUTION: The above output control options are incompatible with each
%%% other.</dd>
%%% <dt>`long_result'</dt>
%%% <dd>Enables long-result mode (see the {@section Counterexamples} section
%%% for details).</dd>
%%% <dt>`{numtests, <Positive_integer>}' or simply `<Positive_integer>'</dt>
%%% <dd>This is equivalent to the {@link numtests/1} property wrapper. Any
%%% {@link numtests/1} wrappers in the actual property will overwrite this
%%% user option.</dd>
%%% <dt>`{start_size, <Size>}'</dt>
%%% <dd>Specifies the initial value of the `size' parameter (default is 1), see
%%% the documentation of the {@link proper_types} module for details.</dd>
%%% <dt>`{max_size, <Size>}'</dt>
%%% <dd>Specifies the maximum value of the `size' parameter (default is 42), see
%%% the documentation of the {@link proper_types} module for details.</dd>
%%% <dt>`{max_shrinks, <Non_negative_integer>}'</dt>
%%% <dd>Specifies the maximum number of times a failing test case should be
%%% shrunk before returning. Note that the shrinking may stop before so many
%%% shrinks are achieved if the shrinking subsystem deduces that it cannot
%%% shrink the failing test case further. Default is 500.</dd>
%%% <dt>`noshrink'</dt>
%%% <dd>Instructs PropEr to not attempt to shrink any failing test cases.</dd>
%%% <dt>`{constraint_tries, <Positive_integer>}'</dt>
%%% <dd>Specifies the maximum number of tries before the generator subsystem
%%% gives up on producing an instance that satisfies a `?SUCHTHAT'
%%% constraint. Default is 50.</dd>
%%% <dt>`fails'</dt>
%%% <dd>This is equivalent to the {@link fails/1} property wrapper.</dd>
%%% <dt>`{spec_timeout, infinity | <Non_negative_integer>}'</dt>
%%% <dd>When testing a spec, PropEr will consider an input to be failing if the
%%% function under test takes more than the specified amount of milliseconds
%%% to return for that input.</dd>
%%% <dt>`any_to_integer'</dt>
%%% <dd>All generated instances of the type {@link proper_types:any/0} will be
%%% integers. This is provided as a means to speed up the testing of specs,
%%% where `any()' is a commonly used type (see the {@section Spec testing}
%%% section for details).</dd>
%%% <dt>`{skip_mfas, [<MFA>]}'</dt>
%%% <dd> When checking a module's specs, PropEr will not test the
%%% specified MFAs. Default is [].</dd>
%%% <dt>`{false_positive_mfas, fun((mfa(),[Arg::term()],{fail, Result::term()} | {error | exit | throw, Reason::term()}) -> boolean()) | undefined}'</dt>
%%% <dd> When checking a module's spec(s), PropEr will treat a
%%% counterexample as a false positive if the user supplied function
%%% returns true. Otherwise, PropEr will treat the counterexample as
%%% it normally does. The inputs to the user supplied function are
%%% the MFA, the arguments passed to the MFA, and the result returned
%%% from the MFA or an exception with it's reason. If needed, the
%%% user supplied function can call erlang:get_stacktrace/0. Default
%%% is undefined.</dd>
%%% <dt>`nocolors'</dt>
%%% <dd>Do not use term colors in output.</dd>
%%% <dt>`{numworkers, <Non_negative_number>}'</dt>
%%% <dd> Specifies the number of workers to spawn when performing the tests (defaults to 0).
%%% Each worker gets their own share of the total of number of tests to perform.</dd>
%%% <dt>`{strategy_fun, <Strategy_function>}'</dt>
%%% <dd> Overrides the default function used to split the load of tests among the workers.
%%% It should be of the type {@link strategy_fun()}.</dd>
%%% <dt>`pure | impure'</dt>
%%% <dd> Declares the type of the property, as in pure with no side-effects or state,
%%% and impure with them. <b>Notice</b>: this option will only be taken into account if
%%% the number of workers set is greater than 0. In addition, <i>impure</i> properties
%%% have each worker spawned on its own node.</dd>
%%% <dt>`{stop_nodes, boolean()}'</dt>
%%% <dd> Specifies whether parallel PropEr should stop the nodes after running a property
%%% or not. Defaults to true.</dd>
%%% </dl>
%%%
%%% == Spec testing ==
%%% You can test the accuracy of an exported function's spec by running
%%% {@link check_spec/1} or {@link check_spec/2}.
%%% Under this mode of operation, PropEr will call the provided function with
%%% increasingly complex valid inputs (according to its spec) and test that no
%%% unexpected value is returned. If an input is found that violates the spec,
%%% it will be saved as a counterexample and PropEr will attempt to shrink it.
%%%
%%% You can test all exported functions of a module against their spec by
%%% running {@link check_specs/1} or {@link check_specs/2}.
%%%
%%% The use of `check_spec' is subject to the following usage rules:
%%%
%%% <ul>
%%% <li>Currently, PropEr can't test functions whose range contains a type
%%% that exhibits a certain kind of self-reference: it is (directly or
%%% indirectly) self-recursive and at least one recursion path contains only
%%% unions and type references. E.g. these types are acceptable:
%%% ``` -type a(T) :: T | {'bar',a(T)}.
%%% -type b() :: 42 | [c()].
%%% -type c() :: {'baz',b()}.'''
%%% while these are not:
%%% ``` -type a() :: 'foo' | b().
%%% -type b() :: c() | [integer()].
%%% -type c() :: 'bar' | a().
%%% -type d(T) :: T | d({'baz',T}).''' </li>
%%% <li>Throwing any exception or raising an `error:badarg' is considered
%%% normal behaviour. Currently, users cannot fine-tune this setting.</li>
%%% <li>Only the first clause of the function's spec is considered.</li>
%%% <li>The only spec constraints we accept are is_subtype' constraints whose
%%% first argument is a simple, non-'_' variable. It is not checked whether or
%%% not these variables actually appear in the spec. The second argument of an
%%% `is_subtype' constraint cannot contain any non-'_' variables. Multiple
%%% constraints for the same variable are not supported.</li>
%%% </ul>
%%%
%%% == Errors ==
%%% The following errors may be encountered during testing. The term provided
%%% for each error is the error type returned by proper:quickcheck in case such
%%% an error occurs. Normally, a message is also printed on screen describing
%%% the error.
%%%
%%% <dl>
%%% <dt>`arity_limit'</dt>
%%% <dd>The random instance generation subsystem has failed to produce
%%% a function of the desired arity. Please recompile PropEr with a suitable
%%% value for `?MAX_ARITY' (defined in `proper_internal.hrl'). This error
%%% should only be encountered during normal operation.</dd>
%%% <dt>`{cant_generate, [<MFA>]}'</dt>
%%% <dd>The random instance generation subsystem has failed to
%%% produce an instance that satisfies some `?SUCHTHAT' constraint. You
%%% should either increase the `constraint_tries' limit, loosen the failing
%%% constraint, or make it non-strict. The failure is due to a failing
%%% strict constraint which is wrapped by one of the MFAs from the list of
%%% candidates `[<MFA>]'.
%%% This error should only be encountered during normal operation.</dd>
%%% <dt>`cant_satisfy'</dt>
%%% <dd>All the tests were rejected because no produced test case
%%% would pass all `?IMPLIES' checks. You should loosen the failing `?IMPLIES'
%%% constraint(s). This error should only be encountered during normal
%%% operation.</dd>
%%% <dt>`non_boolean_result'</dt>
%%% <dd>The property code returned a non-boolean result. Please
%%% fix your property.</dd>
%%% <dt>`rejected'</dt>
%%% <dd>Only encountered during re-checking, the counterexample does not
%%% match the property, since the counterexample doesn't pass an `?IMPLIES'
%%% check.</dd>
%%% <dt>`too_many_instances'</dt>
%%% <dd>Only encountered during re-checking, the counterexample
%%% does not match the property, since the counterexample contains more
%%% instances than there are `?FORALL's in the property.</dd>
%%% <dt>`type_mismatch'</dt>
%%% <dd>The variables' and types' structures inside a `?FORALL' don't
%%% match. Please check your properties.</dd>
%%% <dt>`{typeserver, <SubError>}'</dt>
%%% <dd>The typeserver encountered an error. The `<SubError>' field contains
%%% specific information regarding the error.</dd>
%%% <dt>`{unexpected, <Result>}'</dt>
%%% <dd>A test returned an unexpected result during normal operation. If you
%%% ever get this error, it means that you have found a bug in PropEr
%%% - please send an error report to the maintainers and remember to include
%%% both the failing test case and the output of the program, if possible.
%%% </dd>
%%% <dt>`{erroneous_option, <Option>}'</dt>
%%% <dd>There is something wrong in how `<Option>' is specified by the user;
%%% most likely a value was supplied for it that is not what is expected.</dd>
%%% <dt>`{unrecognized_option, <Option>}'</dt>
%%% <dd>`<Option>' is not an option that PropEr understands.</dd>
%%% </dl>
-module(proper).
-export([quickcheck/1, quickcheck/2, counterexample/1, counterexample/2,
check/2, check/3, module/1, module/2, check_spec/1, check_spec/2,
check_specs/1, check_specs/2]).
-export([numtests/2, fails/1, on_output/2, conjunction/1]).
-export([collect/2, collect/3, aggregate/2, aggregate/3, classify/3, measure/3,
with_title/1, equals/2]).
-export([counterexample/0, counterexamples/0]).
-export([clean_garbage/0, global_state_erase/0]).
-export([test_to_outer_test/1]).
-export([gen_and_print_samples/3]).
-export([get_size/1, global_state_init_size/1,
global_state_init_size_seed/2, report_error/2]).
-export([pure_check/1, pure_check/2]).
-export([forall/2, targeted/2, exists/3, implies/2,
whenfail/2, trapexit/1, timeout/2, setup/2]).
-export_type([test/0, outer_test/0, counterexample/0, exception/0,
false_positive_mfas/0, setup_opts/0]).
-include("proper_internal.hrl").
%%-----------------------------------------------------------------------------
%% Macros
%%-----------------------------------------------------------------------------
-define(MISMATCH_MSG, "Error: The input doesn't correspond to this property: ").
%%-----------------------------------------------------------------------------
%% Color printing macros
%%-----------------------------------------------------------------------------
-define(BOLD_RED, "\033[01;31m").
-define(BOLD_GREEN, "\033[01;32m").
-define(BOLD_YELLOW, "\033[01;33m"). % currently not used
-define(BOLD_BLUE, "\033[01;34m").
-define(BOLD_MAGENTA, "\033[01;35m"). % currently not used
-define(END_MARKER, "\033[00m").
-define(COLOR_WRAP(NoCol, StartMarker, Msg),
case NoCol of
true -> Msg;
false -> StartMarker ++ Msg ++ ?END_MARKER
end).
-define(PRINT(NoCol, StartMarker, Print, Msg, Args),
Print(?COLOR_WRAP(NoCol, StartMarker, Msg), Args)).
%%-----------------------------------------------------------------------------
%% Test types
%%-----------------------------------------------------------------------------
-type imm_testcase() :: [imm_input()].
-type imm_input() :: proper_gen:imm_instance()
| {'$conjunction',sub_imm_testcases()}.
-type sub_imm_testcases() :: [{tag(),imm_testcase()}].
-type imm_counterexample() :: [imm_clean_input()].
-type imm_clean_input() :: proper_gen:instance()
| {'$conjunction',sub_imm_counterexamples()}.
-type sub_imm_counterexamples() :: [{tag(),imm_counterexample()}].
-type counterexample() :: [clean_input()].
%% @alias
-type clean_input() :: proper_gen:instance() | sub_counterexamples().
%% @alias
-type sub_counterexamples() :: [{tag(),counterexample()}].
-type sample() :: [term()].
-type freq_sample() :: [{term(),proper_types:frequency()}].
-type side_effects_fun() :: fun(() -> 'ok').
-type fail_actions() :: [side_effects_fun()].
-type output_fun() :: fun((string(),[term()]) -> 'ok').
%% A fun to be used by PropEr for output printing. Such a fun should follow the
%% conventions of `io:format/2'.
-type tag() :: atom().
-type title() :: atom() | string().
-type stats_printer() :: fun((sample()) -> 'ok')
| fun((sample(),output_fun()) -> 'ok').
%% A stats-printing function that can be passed to some of the statistics
%% collection functions, to be used instead of the predefined stats-printer.
%% Such a function will be called at the end of testing (in case no test fails)
%% with a sorted list of collected terms. A commonly used stats-printer is
%% `with_title/1'.
-type numeric_stats() :: {number(), float(), number()}.
-type time_period() :: non_neg_integer().
-opaque outer_test() :: test()
| {'fails', outer_test()}
| {'setup', setup_fun(), outer_test()}
| {'numtests', pos_integer(), outer_test()}
| {'on_output', output_fun(), outer_test()}.
%% A testable property that has optionally been wrapped with one or
%% more <a href="#external-wrappers">external wrappers</a>.
%% TODO: Should the tags be of the form '$...'?
-opaque test() :: boolean()
| {'forall', proper_types:raw_type(), dependent_test()}
| {'exists', proper_types:raw_type(), dependent_test(), boolean()}
| {'conjunction', [{tag(),test()}]}
| {'implies', boolean(), delayed_test()}
| {'sample', sample(), stats_printer(), test()}
| {'whenfail', side_effects_fun(), delayed_test()}
| {'trapexit', fun(() -> boolean())}
| {'timeout', time_period(), fun(() -> boolean())}.
%%| {'always', pos_integer(), delayed_test()}
%%| {'sometimes', pos_integer(), delayed_test()}
%% A testable property that has not been wrapped with an
%% <a href="#external-wrappers">external wrapper</a>.
-type delayed_test() :: fun(() -> test()).
-type dependent_test() :: fun((proper_gen:instance()) -> test()).
-type lazy_test() :: delayed_test() | dependent_test().
-type raw_test_kind() :: 'test' | 'spec'.
-type raw_test() :: {'test',test()} | {'spec',mfa()}.
-type stripped_test() :: boolean()
| {proper_types:type(), dependent_test()}
| [{tag(),test()}].
-type finalize_fun() :: fun(() -> 'ok').
-type setup_fun() :: fun(() -> finalize_fun())
| fun((setup_opts()) -> finalize_fun()).
-type false_positive_mfas() :: fun((mfa(),Args::[term()],{fail,Result::term()} | {error | exit | throw,Reason::term()}) -> boolean()) | 'undefined'.
-type purity() :: 'pure' | 'impure'.
-type test_range() :: {Start :: non_neg_integer(), ToPass :: pos_integer()}.
-type worker_args() :: test_range() | {node(), test_range()}.
%% Strategy function type
-type strategy_fun() :: fun((NumTests :: pos_integer(), NumWorkers :: pos_integer()) -> [{non_neg_integer(), non_neg_integer()}]).
%% A function that given a number of tests and a number of workers, splits
%% the load in the form of a list of tuples with the first element as the
%% starting test and the second element as the number of tests to do from there on.
%%-----------------------------------------------------------------------------
%% Options and Context types
%%-----------------------------------------------------------------------------
%% TODO: Rename this to 'options()'?
-type user_opt() :: 'any_to_integer'
| 'fails'
| 'long_result'
| 'nocolors'
| 'noshrink'
| purity()
| 'quiet'
| 'verbose'
| pos_integer()
| {'constraint_tries',pos_integer()}
| {'false_positive_mfas',false_positive_mfas()}
| {'max_shrinks',non_neg_integer()}
| {'max_size',proper_gen:size()}
| {'numtests',pos_integer()}
| {'numworkers', non_neg_integer()}
| {'strategy_fun', strategy_fun()}
| {'stop_nodes', boolean()}
| {'on_output',output_fun()}
| {'search_steps',pos_integer()}
| {'search_strategy',proper_target:strategy()}
| {'skip_mfas',[mfa()]}
| {'spec_timeout',timeout()}
| {'start_size',proper_gen:size()}
| {'to_file',io:device()}.
-type user_opts() :: [user_opt()] | user_opt().
-record(opts, {output_fun = fun io:format/2 :: output_fun(),
long_result = false :: boolean(),
numtests = 100 :: pos_integer(),
search_steps = 1000 :: pos_integer(),
search_strategy = proper_sa :: proper_target:strategy(),
start_size = 1 :: proper_gen:size(),
seed = os:timestamp() :: proper_gen:seed(),
max_size = 42 :: proper_gen:size(),
max_shrinks = 500 :: non_neg_integer(),
noshrink = false :: boolean(),
constraint_tries = 50 :: pos_integer(),
expect_fail = false :: boolean(),
any_type :: {'type', proper_types:type()} | 'undefined',
spec_timeout = infinity :: timeout(),
skip_mfas = [] :: [mfa()],
false_positive_mfas :: false_positive_mfas(),
setup_funs = [] :: [setup_fun()],
numworkers = 0 :: non_neg_integer(),
property_type = pure :: purity(),
strategy_fun = default_strategy_fun() :: strategy_fun(),
stop_nodes = true :: boolean(),
parent = self() :: pid(),
nocolors = false :: boolean()}).
-type opts() :: #opts{}.
-record(ctx, {mode = new :: 'new' | 'try_shrunk' | 'try_cexm',
bound = [] :: imm_testcase() | counterexample(),
actions = [] :: fail_actions(),
samples = [] :: [sample()],
printers = [] :: [stats_printer()]}).
-type ctx() :: #ctx{}.
-type setup_opts() :: #{numtests := pos_integer(),
search_steps := pos_integer(),
search_strategy := proper_target:strategy(),
start_size := proper_gen:size(),
max_size := proper_gen:size(),
output_fun := output_fun()}.
%%-----------------------------------------------------------------------------
%% Result types
%%-----------------------------------------------------------------------------
-record(pass, {reason :: pass_reason() | 'undefined',
samples :: [sample()],
printers :: [stats_printer()],
performed :: pos_integer() | 'undefined',
actions :: fail_actions()}).
-record(fail, {reason :: fail_reason() | 'undefined',
bound :: imm_testcase() | counterexample(),
actions :: fail_actions(),
performed :: pos_integer() | 'undefined'}).
%% @alias
-type error() :: {'error', error_reason()}.
-type pass_reason() :: 'true_prop' | 'didnt_crash'.
-type fail_reason() :: 'false_prop' | 'time_out' | {'trapped',exc_reason()}
| exception() | {'sub_props',[{tag(),fail_reason()},...]}
| 'exists' | 'not_found'.
%% @private_type
-type exception() :: {'exception',exc_kind(),exc_reason(),stacktrace()}.
-type exc_kind() :: 'throw' | 'error' | 'exit'.
-type exc_reason() :: term().
-type stacktrace() :: [call_record()].
-type call_record() :: {mod_name(),fun_name(),arity() | list(),location()}.
-type location() :: [{atom(),term()}].
-type error_reason() :: 'arity_limit' | {'cant_generate',[mfa()]}
| 'cant_satisfy'
| 'non_boolean_result' | 'rejected' | 'too_many_instances'
| 'type_mismatch' | 'wrong_type' | {'typeserver',term()}
| {'unexpected',any()} | {'erroneous_option',user_opt()}
| {'unrecognized_option',term()}.
-type run_result() :: #pass{performed :: 'undefined'}
| #fail{performed :: 'undefined'}
| error().
-type imm_result() :: #pass{reason :: 'undefined'} | #fail{} | error().
-type long_result() :: 'true' | counterexample() | error().
-type short_result() :: boolean() | error().
-type result() :: long_result() | short_result().
-type long_module_result() :: [{mfa(),counterexample()}] | error().
-type short_module_result() :: [mfa()] | error().
-type module_result() :: long_module_result() | short_module_result().
-type shrinking_result() :: {non_neg_integer(),imm_testcase()}.
%%-----------------------------------------------------------------------------
%% State handling functions
%%-----------------------------------------------------------------------------
-spec grow_size(opts()) -> 'ok'.
grow_size(#opts{max_size = MaxSize} = Opts) ->
Size = get('$size'),
case Size < MaxSize of
true ->
case get('$left') of
0 ->
{ToRun, NextSize} = tests_at_next_size(Size, Opts),
put('$size', NextSize),
put('$left', ToRun - 1),
ok;
Left ->
put('$left', Left - 1),
ok
end;
false ->
ok
end.
-spec tests_at_next_size(proper_gen:size(), opts()) ->
{pos_integer(), proper_gen:size()}.
tests_at_next_size(_Size, #opts{numtests = 1, start_size = StartSize}) ->
{1, StartSize};
tests_at_next_size(Size, #opts{numtests = NumTests, start_size = StartSize,
max_size = MaxSize})
when Size < MaxSize, StartSize =< MaxSize, NumTests > 1 ->
SizesToTest = MaxSize - StartSize + 1,
case NumTests >= SizesToTest of
true ->
TotalOverflow = NumTests rem SizesToTest,
NextSize = erlang:max(StartSize, Size + 1),
Overflow = case NextSize - StartSize < TotalOverflow of
true -> 1;
false -> 0
end,
{NumTests div SizesToTest + Overflow, NextSize};
false ->
EverySoManySizes = (SizesToTest - 1) div (NumTests - 1),
NextSize =
case Size < StartSize of
true ->
StartSize;
false ->
PrevMultiple =
Size - (Size - StartSize) rem EverySoManySizes,
PrevMultiple + EverySoManySizes
end,
{1, NextSize}
end.
-spec size_at_nth_test(non_neg_integer(), opts()) -> proper_gen:size().
size_at_nth_test(NumTest, #opts{max_size = MaxSize, start_size = StartSize,
numtests = NumTests}) ->
SizesToTest = MaxSize - StartSize + 1,
Size = case NumTests >= SizesToTest of
true ->
Div = NumTests div SizesToTest,
Rem = NumTests rem SizesToTest,
case NumTest < Rem * (Div + 1) of
true ->
NumTest div (Div + 1) + StartSize;
false ->
(NumTest div 2) - (Rem div Div) + StartSize
end;
false ->
case NumTest =:= 0 of
true -> StartSize;
false ->
Diff = (SizesToTest - 1) div (NumTests - 1),
NumTest * Diff + StartSize
end
end,
min(MaxSize, Size).
%% @private
-spec get_size(proper_types:type()) -> proper_gen:size() | 'undefined'.
get_size(Type) ->
case get('$size') of
undefined ->
undefined;
Size ->
case proper_types:find_prop(size_transform, Type) of
{ok,Transform} -> Transform(Size);
error -> Size
end
end.
%% @private
-spec global_state_init_size(proper_gen:size()) -> 'ok'.
global_state_init_size(Size) ->
global_state_init(#opts{start_size = Size}).
%% @private
-spec global_state_init_size_seed(proper_gen:size(), proper_gen:seed()) -> 'ok'.
global_state_init_size_seed(Size, Seed) ->
global_state_init(#opts{start_size = Size, seed = Seed}).
-spec global_state_init(opts()) -> 'ok'.
global_state_init(#opts{start_size = StartSize, constraint_tries = CTries,
search_strategy = Strategy, search_steps = SearchSteps,
any_type = AnyType, seed = Seed, numworkers = NumWorkers} = Opts) ->
clean_garbage(),
put('$size', StartSize - 1),
put('$left', 0),
put('$search_strategy', Strategy),
put('$search_steps', SearchSteps),
grow_size(Opts),
put('$constraint_tries', CTries),
put('$any_type', AnyType),
put('$property_id', erlang:unique_integer()),
put('$proper_test_incr', NumWorkers),
{_, _, _} = Seed, % just an assertion
proper_arith:rand_restart(Seed),
proper_typeserver:restart(),
ok.
-spec global_state_reset(opts()) -> 'ok'.
global_state_reset(#opts{start_size = StartSize} = Opts) ->
clean_garbage(),
put('$size', StartSize - 1),
put('$left', 0),
grow_size(Opts).
%% @private
-spec global_state_erase() -> 'ok'.
global_state_erase() ->
proper_typeserver:stop(),
proper_arith:rand_stop(),
erase('$any_type'),
erase('$constraint_tries'),
erase('$left'),
erase('$size'),
erase('$parameters'),
erase('$search_strategy'),
erase('$search_steps'),
erase('$property_id'),
erase('$proper_test_incr'),
ok.
-spec setup_test(opts()) -> [finalize_fun()].
setup_test(#opts{output_fun = OutputFun,
numtests = NumTests,
search_steps = SearchSteps,
search_strategy = Strategy,
start_size = StartSize,
max_size = MaxSize,
setup_funs = Funs}) ->
SetupOpts = #{numtests => NumTests,
search_steps => SearchSteps,
search_strategy => Strategy,
start_size => StartSize,
max_size => MaxSize,
output_fun => OutputFun},
[case erlang:fun_info(Fun, arity) of
{arity, 0} -> Fun();
{arity, 1} -> Fun(SetupOpts)
end || Fun <- Funs].
-spec finalize_test([finalize_fun()]) -> 'ok'.
finalize_test(Finalizers) ->
lists:foreach(fun (Fun) -> ok = Fun() end, Finalizers).
%% @private
-spec spawn_link_migrate(node(), fun(() -> 'ok')) -> pid().
spawn_link_migrate(Node, ActualFun) ->
PDictStuff = get(),
Fun = fun() ->
lists:foreach(fun({K,V}) -> put(K,V) end, PDictStuff),
proper_arith:rand_reseed(),
ok = ActualFun()
end,
case Node of
undefined ->
spawn_link(Fun);
Node ->
spawn_link(Node, Fun)
end.
-spec save_counterexample(counterexample()) -> 'ok'.
save_counterexample(CExm) ->
put('$counterexample', CExm),
ok.
%% @doc Retrieves the last (simplest) counterexample produced by PropEr during
%% the most recent testing run.
-spec counterexample() -> counterexample() | 'undefined'.
counterexample() ->
get('$counterexample').
-spec save_counterexamples([{mfa(),counterexample()}]) -> 'ok'.
save_counterexamples(CExms) ->
put('$counterexamples', CExms),
ok.
%% @doc Returns a counterexample for each failing property of the most recent
%% module testing run.
-spec counterexamples() -> [{mfa(),counterexample()}] | 'undefined'.
counterexamples() ->
get('$counterexamples').
%% @doc Cleans up the process dictionary of all PropEr-produced entries.
-spec clean_garbage() -> 'ok'.
clean_garbage() ->
erase('$counterexample'),
erase('$counterexamples'),
ok.
%%-----------------------------------------------------------------------------
%% Public interface functions
%%-----------------------------------------------------------------------------
%% @doc Runs PropEr on the property `OuterTest'.
-spec quickcheck(outer_test()) -> result().
quickcheck(OuterTest) ->
quickcheck(OuterTest, []).
%% @doc Same as {@link quickcheck/1}, but also accepts a list of options.
-spec quickcheck(outer_test(), user_opts()) -> result().
quickcheck(OuterTest, UserOpts) ->
try parse_opts(UserOpts) of
ImmOpts ->
{Test,Opts} = peel_test(OuterTest, ImmOpts),
test({test,Test}, Opts)
catch
throw:{Err,_Opt} = Reason when Err =:= erroneous_option;
Err =:= unrecognized_option ->
report_error(Reason, fun io:format/2),
{error, Reason}
end.
%% @equiv quickcheck(OuterTest, [long_result])
-spec counterexample(outer_test()) -> long_result().
counterexample(OuterTest) ->
counterexample(OuterTest, []).
%% @doc Same as {@link counterexample/1}, but also accepts a list of options.
-spec counterexample(outer_test(), user_opts()) -> long_result().
counterexample(OuterTest, UserOpts) ->
quickcheck(OuterTest, add_user_opt(long_result, UserOpts)).
%% @private
%% @doc Runs PropEr in pure mode. Under this mode, PropEr will perform no I/O
%% and will not access the caller's process dictionary in any way. Please note
%% that PropEr will not actually run as a pure function under this mode.
-spec pure_check(outer_test()) -> result().
pure_check(OuterTest) ->
pure_check(OuterTest, []).
%% @private
%% @doc Same as {@link pure_check/2}, but also accepts a list of options.
-spec pure_check(outer_test(), user_opts()) -> result().
pure_check(OuterTest, ImmUserOpts) ->
Parent = self(),
UserOpts = add_user_opt(quiet, ImmUserOpts),
spawn_link(fun() -> Parent ! {result, quickcheck(OuterTest, UserOpts)} end),
receive
{result, Result} -> Result
end.
%% @doc Tests the accuracy of an exported function's spec.
-spec check_spec(mfa()) -> result().
check_spec(MFA) ->
check_spec(MFA, []).
%% @doc Same as {@link check_spec/1}, but also accepts a list of options.
-spec check_spec(mfa(), user_opts()) -> result().
check_spec(MFA, UserOpts) ->
try parse_opts(UserOpts) of
Opts ->
test({spec,MFA}, Opts)
catch
throw:{Err,_Opt} = Reason when Err =:= erroneous_option;
Err =:= unrecognized_option ->
report_error(Reason, fun io:format/2),
{error, Reason}
end.
%% @doc Re-checks a specific counterexample `CExm' against the property
%% `OuterTest' that it previously falsified.
-spec check(outer_test(), counterexample()) -> short_result().
check(OuterTest, CExm) ->
check(OuterTest, CExm, []).
%% @doc Same as {@link check/2}, but also accepts a list of options.
-spec check(outer_test(), counterexample(), user_opts()) -> short_result().
check(OuterTest, CExm, UserOpts) ->
try parse_opts(UserOpts) of
ImmOpts ->
{Test,Opts} = peel_test(OuterTest, ImmOpts),
retry(Test, CExm, Opts)
catch
throw:{Err,_Opt} = Reason when Err =:= erroneous_option;
Err =:= unrecognized_option ->
report_error(Reason, fun io:format/2),
{error, Reason}
end.
%% @doc Tests all properties (i.e., all 0-arity functions whose name begins with
%% `prop_') exported from module `Mod'.
-spec module(mod_name()) -> module_result().
module(Mod) ->
module(Mod, []).
%% @doc Same as {@link module/1}, but also accepts a list of options.
-spec module(mod_name(), user_opts()) -> module_result().
module(Mod, UserOpts) ->
multi_test_prep(Mod, test, UserOpts).
%% @doc Tests all exported, `-spec'ed functions of a module `Mod' against their
%% spec.
-spec check_specs(mod_name()) -> module_result().
check_specs(Mod) ->
check_specs(Mod, []).
%% @doc Same as {@link check_specs/1}, but also accepts a list of options.
-spec check_specs(mod_name(), user_opts()) -> module_result().
check_specs(Mod, UserOpts) ->
multi_test_prep(Mod, spec, UserOpts).
-spec multi_test_prep(mod_name(), raw_test_kind(), user_opts()) ->
module_result().
multi_test_prep(Mod, Kind, UserOpts) ->
try parse_opts(UserOpts) of
Opts ->
multi_test(Mod, Kind, Opts)
catch
throw:{Err,_Opt} = Reason when Err =:= erroneous_option;
Err =:= unrecognized_option ->
report_error(Reason, fun io:format/2),
{error, Reason}
end.
%% @doc A type-conversion function that can be used to convert an argument of
%% a {@type proper:test()} opaque type to a {@type proper:outer_test()} opaque
%% type so that the latter type can be passed to functions such as
%% {@link proper:quickcheck/1} without a warning from dialyzer.
-spec test_to_outer_test(test()) -> outer_test().
test_to_outer_test(Test) -> Test.
%%-----------------------------------------------------------------------------
%% Options parsing functions
%%-----------------------------------------------------------------------------
-spec add_user_opt(user_opt(), user_opts()) -> [user_opt(),...].
add_user_opt(NewUserOpt, UserOptsList) when is_list(UserOptsList) ->
[NewUserOpt | UserOptsList];
add_user_opt(NewUserOpt, SingleUserOpt) ->
add_user_opt(NewUserOpt, [SingleUserOpt]).
-spec parse_opts(user_opts()) -> opts().
parse_opts(UserOptsList) when is_list(UserOptsList) ->
parse_opts(lists:reverse(UserOptsList), maybe_override_numworkers(#opts{}));
parse_opts(SingleUserOpt) ->