Since the last gen_fsm test post already tip-toed on the subject of Automated Testing, I thought it would be natural to go into QuickCheck and “bring out the big” guns.

Enter QuickCheck.

## What is quickcheck?

QuickCheck for Erlang is a commercial tool from QuviQ for *Property Based Testing* by automatic generation of testdata that is fed into property specifications. Behind this we find John Hughes and Thomas Arts. Written in Erlang.

For the Haskell fans out there, I hope you recognize QuickCheck from the Haskell history, through this incredibly well-designed page (irony). *As a side-note, I did firewall testing with the Haskell QuickCheck some time ago for a company called Witsbits*.

This post will use the free QuickCheck mini version.

## How do I install it?

This is seriously *easy*, and takes under 10 seconds (no honestly). **Unzip the eqcmini.zip** archive and you have your “installation”. As the product is shipped with the beamfiles, you don’t need to (you actually can’t) compile anything.

## How do I use it?

You need three things in order to get QuickChecking (qc’ing : queue-see-ing)

- A module including the quickcheck application header file,
**-include_lib(“eqc/include/eqc.hrl”).** - Inside the same module,
**properties**you will run your test on, each property must be exported. - A module with the actual implementation of what we wish to test.

This is very similar as to EUnit testing. We have a test-module consisting of tests and the EUnit header file, and an implementation file with the actual code.

The idea is that the test module exports the properties that will be tested by quickcheck.

## How can I do TDD with QuickCheck?

For the purpose of this example, we shall develop parts of a small clock library that makes it possible to add / subtract time with its basis in the time() format.

As usual, we will probably a standard layout with the minimals, ebin/ src/ test/ and a makefile.

zen:QCMini zenon$ tree -L 2. . ├── Makefile ├── ebin ├── lib │ └── eqc-1.0.1 ├── src │ └── clock.erl └── test └── clock_eqc.erl 5 directories, 3 files

As can be seen, the quickcheck directory is put into the lib/ directory, and I keep the now empty clock module in src/ with the test module in test/

The clock_eqc.erl contains the following initial code

-module(clock_eqc). -include_lib("eqc/include/eqc.hrl"). -compile(export_all). prop_time_to_seconds() -> ?FORALL({H,M,S},{nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, clock:hms2s({H,M,S}) == (H*60*60)+(M*60)+S)))).

First we see that the the property has arity 0 (zero). The name also begins with prop_. The *?FORALL* is a quickcheck macro

?FORALL(X,Gen,Prop)

with the first element being the pattern; in this case the 3-tuple {H, M, S} which will be pattern matched for value binding to generated values from the Generator. The second element is the Generator from where values (3-tuple of natural numbers) are generated and bound to the Pattern and the third being the *Property*. For this example, the property is everything from the next line (?IMPLIES…) to the end.

The ?IMPLIES macro has two elements. A precondition (for this example: the (H < 24)) works as a filter, only allowing H values with values in the range 1 – 23, it discard all tests for which the precondition does not hold and runs the tests for which the precondition is valid. Second element is the Property (for this exmple: everything from ?IMPLIES(M < 60)… and onward).

For this code piece, we see that there is one Pattern and generator, three natural numbers, then 3 preconditions, ensuring that only sane values are given for (H)ours, (M)inutes and (S)econds. When the sifted values are accepted, the last part can be thought of as the property: The function call hms2s/1 must return the amount of seconds for the 3-tuple. Here we are doing a crucial thing, which is basic to quickcheck. We are comparing the function value with our *model*.

The clock.erl module is totally blank except for the module declaration, and the Make file holds

QCLIB := lib/eqc-1.0.1/ebin/ all: erlc -o ebin/ -pa $(QCLIB) src/*.erl test/*.erl .PHONY: test test: all erl -pa ebin/ -pa $(QCLIB) -eval 'eqc:module(clock_eqc).'

Let’s run the first *make test (with trunkated output)*

zen:QCMini zenon$ make test 1> prop_time_to_seconds: Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}}) Failed! Reason: {'EXIT',{undef,[{clock,hms2s,[{0,0,0}]}, {clock_eqc,'-prop_time_to_seconds/0-fun-0-',3}, {eqc,implies,3}, {eqc,'-f885_0/2-fun-4-',2}, {eqc_gen,'-f330_0/2-fun-0-',5}, {eqc_gen,f195_0,2}, {eqc_gen,gen,3}, {eqc,'-f867_0/1-fun-2-',3}]}} After 1 tests. {0,0,0} 1>

Not too unexpected, there is no function hms2s exported. Let’s write and export it.

-module(clock). -export([hms2s/1]). hms2s({H,M,S}) -> H*60*60 + M*60 + S.

Now, let’s run test

zen:QCMini zenon$ make test 1> prop_time_to_seconds: Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}}) ................................................................... ...........x......xx.......x.....x.x... OK, passed 100 tests 1>

Passed 100, seems good. The ‘x’ we see are cases that where discarded due to failed preconditions (H < 24, M < 60, S < 60).

Next test, we want to do the same for minutes and hours (only showing the isolated tests in themselves, not the whole module each time).

prop_time_to_minutes() -> ?FORALL({H,M,S},{nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, clock:hms2m({H,M,S}) == (H*60)+M+S/60)))).

And the trivial implementation (leaving out rest of module)

hms2m({H,M,S}) -> H*60+M+S/60.

with running

zen:QCMini zenon$ make test Eshell V5.8.1 (abort with ^G) 1> prop_time_to_seconds: Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}}) ................................................................... ............x..........xxx..x........x. OK, passed 100 tests prop_time_to_minutes: ............................................... .........................................x............ OK, passed 100 tests 1>

As the last in the trio goes, hms2h left, after that one, we will implement the converse functions, returning time() type tuples from (H)ours, (M)inutes and (S)econds.

In good TDD style, first the test.

prop_time_to_hours() -> ?FORALL({H,M,S},{nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, clock:hms2h({H,M,S}) == H+M/60+(S/(60*60)))))).

and then the implementation

hms2h({H,M,S}) -> H+(M/60)+(S/(60*60)).

Now for the reverse functions, of course, the test first, in true TDD

prop_seconds_to_time() -> ?FORALL(S,nat(), begin S2 = S rem 60, M = (S div 60) rem 60, H = (S div 60) div 60, clock:s2hms(S) == {H,M,S2} end).

A very interesting thing we see from the above code is that when doing property driven development is that in developing the model for the property, one may find the solution to the implementation. In contrast to EUnit tests, this is one step closer to the implementation.

s2hms(S) -> {(S div 60) div 60, (S div 60) rem 60, S rem 60}.

And so the test run

zen:QCMini zenon$ make test Eshell V5.8.1 (abort with ^G) 1> prop_time_to_seconds: Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}}) ............................................................. ......................x......x.....x..x..x.xx. OK, passed 100 tests prop_time_to_minutes: .......................................... ..............................x......xx....x...xx.xx..........x.... OK, passed 100 tests prop_time_to_hours: ........................................... ....................................x.....x.x...x.........x... OK, passed 100 tests prop_seconds_to_time: ........................................... ......................................................... OK, passed 100 tests

Now, I will do a quick fast forward for the rest of the reverse functions, m2hms/1 and h2hms/1. I will present the tests and the solutions.

prop_minutes_to_time() -> ?FORALL(M,nat(), begin H = M div 60, M2= M rem 60, clock:m2hms(M) == {H,M2,0} end). prop_hours_to_time() -> ?FORALL(H, nat(), clock:h2hms(H) == {H,0,0}).

And the implementation that can trivially be taken from the model

m2hms(M) -> {M div 60, M rem 60, 0}. h2hms(H) -> {H,0,0}.

You can take my word for that this will pass the tests, or try it yourself with make test. Next is the addition and subtraction functions. They will allow us to subtract and add seconds, minutes and hours from a given time() 3-tuple.

First, we write a test, based on the previously (seemingly) okay functions, for the internal model

prop_subtract_seconds_from_time() -> ?FORALL({H,M,S,S2},{nat(),nat(),nat(),nat()}, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H < 24, ?IMPLIES(S2 =< ((H*60*60)+(M*60)+S), begin T = {H,M,S}, clock:sub_sec(T,S2) == clock:s2hms((clock:hms2s(T) - S2)) end))))).

Here we see that some sanity is made sure of, by never subtracting more time than possible from a time(), with the final precondition. I now purposefully write some dirty code for this

sub_sec({H,M,S},S2) -> Hsub = (S div 60) div 60, Msub = S2 div 60, Ssub = S2 rem 60, { H - Hsub, M - Msub, S - Ssub }.

Oh! The test fails, and I remove all the other output that was okay

zen:QCMini zenon$ make test 1> prop_subtract_seconds_from_time: ......Failed! After 7 tests. {1,0,1,2} Shrinking..(2 times) {1,0,0,1}

Here we see that QuickCheck generated a minimal failing case with Hour = 1, Minutes = 0, Seconds = 0 and Subtracting 1 second fails. Using these values with the model (in the console)

1> clock:s2hms((clock:hms2s({1,0,0}) - 1)). {0,59,59} 2>

we see that the model seems sane. Removing one second from an hour produces 59 minutes and 59 seconds. All okay. Now what about my broken implementation? Well, obviously it did not account for “lending”. Since we want the actual implementation to be quicker than the model, it would be cheating to copy the model.

Some coding

sub_sec({H,M,S},S2) -> Sres = S - (S2 rem 60), Mres = M - (S2 div 60), Hres = H - (M div 60), case {Sres < 0, Mres > 0, Mres == 0} of {false,false,false} -> {Hres - 1, Mres+60, Sres}; {true,true,_} -> {Hres, Mres - 1, Sres + 60}; {true,false,_} -> {Hres - 1, Mres + 59, Sres + 60}; _ -> {Hres,Mres,Sres} end.

and the test

zen:QCMini zenon$ make test Eshell V5.8.1 (abort with ^G) 1> prop_time_to_seconds: Starting eqc mini version 1.0.1 (compiled at {{2010,6,13},{11,15,30}}) prop_subtract_seconds_from_time: ..............................x.......... .....................................xxx..xx...............x.x..xx... OK, passed 100 tests

Yes. Nice! But how sure are we that this is not running trivial tests? Well, just check WHAT it is testing, by *collect*ing the testdata! Note the added eqc:collect/2 function for the line after the last precondition.

prop_subtract_seconds_from_time() -> ?FORALL({H,M,S,S2},{nat(),nat(),nat(),nat()}, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H < 24, ?IMPLIES(S2 =< ((H*60*60)+(M*60)+S), eqc:collect({H,M,S,S2}, begin T = {H,M,S}, clock:sub_sec(T,S2) == clock:s2hms((clock:hms2s(T) - S2)) end)))))).

Running the tests should now spew a lot of test statistics similar to this

OK, passed 100 tests 3% {0,0,0,0} 2% {3,3,0,2} 1% {22,23,28,21} 1% {21,6,24,1} 1% {20,15,13,11} 1% {20,6,8,27} 1% {20,0,9,12} 1% {19,25,30,29} 1% {19,18,9,7} 1% {18,13,25,25} .....

with A LOT of lines, so if you don’t trust your model OR your implementation, you are welcome to check out the used values by hand. For now, we are good.

I hope this first post on QuickCheck shows that you CAN do TDD with QuickCheck and also wet your appetite for QC if it was your first encounter with it. Next time I will continue on this clock lib and try to show more QC stuff.

Cheers

/G

## Andre

/ November 10, 2010There’s also Triq, an open source eqc implementation.

## reputation management

/ May 3, 2013Having read this I thought it was extremely informative.

I appreciate you taking the time and energy to put this information

together. I once again find myself spending a lot

of time both reading and leaving comments. But so what, it was still worthwhile!