As a continuation on the QuickCheck series, we will now make a serious attempt at refactoring – tests and implementation. First of the much repeated test-code where the generated properties to often fail the preconditions.

Don’t see what I mean? Take a look at the nought and crosses pattern after a ‘make test’

Now, our first adjustment will be to replace the common pattern

{nat(),nat(),nat()}

for our own homegrown generator. The goal is to have a generator which gives us {H,M,S} values within the ranges of reasonable values (0 – 24 system). Defining our own generators is quite easy, we just define a function which returns a 3-tuple. Now, our first generator in this example is a function of arity zero, qctime/0.qctime/0 will return a 3-tuple containing values matching the 24h format. Thus, we implementit with the help of eqc_gen (the QuickCheck generator library) as follows

qctime() -> {eqc_gen:choose(0,23), eqc_gen:choose(0,59), eqc_gen:choose(0,59)}.

The eqc_gen:choose/2 function will randomly generate a number in the range (inclusive) of the arguments given. Every time you write your own generator, it is a good idea to try it out for yourself in the console with the eqc_gen:sample/1 function. The eqc_gen:sample/1 takes a generator as an argument and gives you a sample of what it generates.

eqc_gen:sample({eqc_gen:choose(0,23), eqc_gen:choose(0,59), eqc_gen:choose(0,59)}).

We can easily try it out after a ‘make test’ run or by forcing a start as

zen:QCMini zenon$ erl -pa lib/eqc-1.0.1/ebin/ Erlang R14B (erts-5.8.1) [source] [smp:4:4] [rq:4] [async-threads:0] [hipe] [kernel-poll:false] Eshell V5.8.1 (abort with ^G) 1> eqc_gen:sample({eqc_gen:choose(0,23), 1> eqc_gen:choose(0,59), 1> eqc_gen:choose(0,59)}). {2,45,25} {0,18,49} {13,25,36} {3,51,44} {16,44,39} {16,11,32} {20,19,24} {21,15,1} {23,21,38} {12,36,0} {15,8,21} ok

Looking good. All seems in order here. Replacing all the pesky {nat(),nat(),nat()} is now the next step. As we replace them, we can also remove all the preconditions that previously”filtered” their values, so remove all the ?IMPLIES(H < 24, … , ?IMPLIES(S < 60 as well.The change is great as our tests become much more readable. From

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)))).

to

prop_time_to_seconds() -> ?FORALL({H,M,S},qctime(), clock:hms2s({H,M,S}) == (H*60*60)+(M*60)+S).

However, this will only remove the majority of the duplication. There are still some cases which have some preconditions causing a lot of the properties to be sieved away. The subtrac properties require the subtraction to result in a positive or zero value result, this we can remedy with a value-dependent generator.

qcLT(X) -> eqc_gen:choose(0,X).

Similary we can tuck away the other ?IMPLIES preconditions with smart generators. For the case of prop_subtract_seconds_from_time/0, we write a generator that takes a time/0 3-tuple as argument and returns an appropriate second value for it.

qcLTs({H,M,S}) -> eqc_gen:choose(0,H*3600 + M*60 + S).

Now the test can be rewritten from

prop_subtract_seconds_from_time() -> ?FORALL({{H,M,S},S2},{qctime(),nat()}, ?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)).

to

prop_subtract_seconds_from_time() -> ?FORALL(Time,qctime(), ?FORALL(Sec,qcLTs(Time), begin clock:sub_sec(Time,Sec) == clock:s2hms((clock:hms2s(Time) - Sec)) end)).

As we run the tests frequently while making the changes, we will now observe that the newer and better QuickCheck module helped us find a bug!

zen:QCMini zenon$ make test prop_subtract_seconds_from_time: Failed! After 1 tests. {3,2,58} 10172 Shrinking...........(11 times) {2,0,0} 3601

The output shows that the generated values {2,0,0} together with 3601 will make the test fail. So, if we subtract 3601 seconds from 2 Hours, we would suspect to see the wrong result

1> clock:sub_sec({2,0,0},3601). {1,-1,59}

And indeed this does look fishy. Taking a second look at the implementation it does look gritty, and a better implementation will be written in a hand-turn (swedish expression)

-spec(sub_sec(time(), nat()) -> time()). sub_sec(T,S) -> sub2(h,sub2(m,sub2(s,{T,S}))).

it relies on the newly added function

sub2(s,{{H,M,S},S2}) -> Ssub = S2 rem 60, {case {Ssub > S andalso M > 0, Ssub > S andalso M == 0} of {true,_} -> {H,M-1,S+60-Ssub}; {_,true} -> {H-1,M+59,S+60-Ssub}; _ -> {H,M,S-Ssub} end,(S2 - Ssub) div 60}; sub2(m,{{H,M,S},M2}) -> Msub = M2 rem 60, {case Msub > M andalso H > 0 of true -> {H-1,M+60-Msub,S}; false ->{H,M-Msub,S} end,(M2 - Msub) div 60}; sub2(h,{{H,M,S},H2}) -> {H-H2,M,S}.

Running the tests will now pass. sub2/2 is written so as to be composable, making each subtraction for seconds and minutes easier.

Now for another fix in the quickcheck module. There are still too many failed predicates for the prop_sub_time test. Running it will most likely give an output of mostly ‘x’ and some ‘.’, this is due to the failed precondition

?IMPLIES(((H*3600) + M*60 + S) >= ((H2*3600) + M2*60 + S2),

Similarly as for the previous test that needs the generated value to be less than the first argument of a subtraction, we can have a dependant generator for the 3-tuple

qcLTt({H,M,S}) -> {eqc_gen:choose(0,H), eqc_gen:choose(0,M), eqc_gen:choose(0,S)}.

This generator will guarantee to generate a time() tuple which is less than or equal to the given one. Problem solved, we can now rewrite the test

prop_sub_time() -> eqc:numtests(100, ?FORALL({{H,M,S},{H2,M2,S2}},{qctime(),qctime()}, ?IMPLIES(((H*3600) + M*60 + S) >= ((H2*3600) + M2*60 + S2), begin T = {H,M,S}, T2= {H2,M2,S2}, clock:sub(T,T2) == clock:s2hms(clock:hms2s(T) - clock:hms2s(T2)) end))).

to

prop_sub_time() -> ?FORALL(T,qctime(), ?FORALL(T2,qcLTt(T), begin clock:sub(T,T2) == clock:s2hms(clock:hms2s(T) - clock:hms2s(T2)) end)).

Running the tests should now show the following

zen:QCMini zenon$ make test erlc -o ebin/ -pa lib/eqc-1.0.1/ebin/ src/*.erl test/*.erl erl -pa ebin/ -pa lib/eqc-1.0.1/ebin/ -eval 'eqc:module(clock_eqc).' Erlang R14B (erts-5.8.1) [source] [smp:4:4] [rq:4] [async-threads:0] [hipe] [kernel-poll:false] 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}}) .................................................................. .................................. OK, passed 100 tests prop_time_to_minutes: .............................................. ...................................................... OK, passed 100 tests prop_time_to_hours: ............................................... ..................................................... OK, passed 100 tests prop_seconds_to_time: .............................................. ...................................................... OK, passed 100 tests prop_minutes_to_time: .............................................. ...................................................... OK, passed 100 tests prop_hours_to_time: ................................................ .................................................... OK, passed 100 tests prop_subtract_seconds_from_time: ..................................... ............................................................... OK, passed 100 tests prop_subtract_hours_from_time: ....................................... ............................................................. OK, passed 100 tests prop_subtract_minutes_from_time: ..................................... ............................................................... OK, passed 100 tests prop_add_time: .................................................... ................................................ OK, passed 100 tests prop_sub_time: .................................................... ................................................ OK, passed 100 tests 1>

Perfect. The tests are now readable and make more sense. We even found a bug in the original implementation.

We have now seen how to write simple generators with arity zero, dependant generators that take generated values as arguments and how this helps us reduce the size of the test code as well as make it more readable.

Now follow the final quickcheck implementation with the final code

# clock_eqc.erl

%%% @author Gianfranco <zenon@zen.home> %%% @copyright (C) 2010, Gianfranco %%% Created : 21 Nov 2010 by Gianfranco <zenon@zen.home> -module(clock_eqc). -include_lib("eqc/include/eqc.hrl"). -compile(export_all). % --------------------------------------------------------------- qctime() -> {eqc_gen:choose(0,23), eqc_gen:choose(0,59), eqc_gen:choose(0,59)}. qcLT(X) -> eqc_gen:choose(0,X). qcLTs({H,M,S}) -> eqc_gen:choose(0,(H*3600)+ (M*60) + S). qcLTm({H,M,S}) -> eqc_gen:choose(0,H*60+M). qcLTt({H,M,S}) -> {eqc_gen:choose(0,H), eqc_gen:choose(0,M), eqc_gen:choose(0,S)}. prop_time_to_seconds() -> ?FORALL({H,M,S},qctime(), clock:hms2s({H,M,S}) == (H*60*60)+(M*60)+S). prop_time_to_minutes() -> ?FORALL({H,M,S},qctime(), clock:hms2m({H,M,S}) == (H*60)+M+S div 60). prop_time_to_hours() -> ?FORALL({H,M,S},qctime(), clock:hms2h({H,M,S}) == H+(M div 60)+(S div (60*60))). prop_seconds_to_time() -> ?FORALL(S,nat(), begin S2= S rem 60, M = (S div 60) rem 60, H = ((S div 60) div 60) rem 24, clock:s2hms(S) == {H,M,S2} end). prop_minutes_to_time() -> ?FORALL(M,nat(), begin H = (M div 60) rem 24, M2= M rem 60, clock:m2hms(M) == {H,M2,0} end). prop_hours_to_time() -> ?FORALL(H, nat(), clock:h2hms(H) == {H rem 24,0,0}). prop_subtract_seconds_from_time() -> ?FORALL(Time,qctime(), ?FORALL(Sec,qcLTs(Time), begin clock:sub_sec(Time,Sec) == clock:s2hms((clock:hms2s(Time) - Sec)) end)). prop_subtract_hours_from_time() -> eqc:numtests(100, ?FORALL({H,M,S},qctime(), ?FORALL(H2,qcLT(H), begin clock:sub_hour({H,M,S},H2) == {H-H2,M,S} end))). prop_subtract_minutes_from_time() -> ?FORALL(T,qctime(), ?FORALL(M,qcLTm(T), begin clock:sub_minute(T,M) == clock:s2hms((clock:hms2s(T) - (M*60))) end)). prop_add_time() -> ?FORALL({{H,M,S},{H2,M2,S2}},{qctime(),qctime()}, begin T = {H,M,S}, T2= {H2,M2,S2}, {HRes,MRes,SRes} = clock:add(T,T2), HRes < 24 andalso MRes < 60 andalso SRes < 60 andalso {HRes,MRes,SRes} == clock:s2hms(clock:hms2s(T) + clock:hms2s(T2)) end). prop_sub_time() -> ?FORALL(T,qctime(), ?FORALL(T2,qcLTt(T), begin clock:sub(T,T2) == clock:s2hms(clock:hms2s(T) - clock:hms2s(T2)) end)).

After the implementation in clock.erl some changes where made to that one as well, and the final module is presented below

# clock.erl

%%% @author Gianfranco <zenon@zen.home> %%% @copyright (C) 2010, Gianfranco %%% Created : 21 Nov 2010 by Gianfranco <zenon@zen.home> -module(clock). -export([ hms2s/1,hms2m/1,hms2h/1, s2hms/1,m2hms/1,h2hms/1, sub_sec/2,sub_hour/2,sub_minute/2, add/2,sub/2 ]). -type nat() :: non_neg_integer(). -type time() :: {nat(),nat(),nat()}. -spec(hms2s(time()) -> nat()). hms2s({H,M,S}) -> H*3600 + M*60 + S. -spec(hms2m(time()) -> nat()). hms2m({H,M,S}) -> H*60+M+(S div 60). -spec(hms2h(time()) -> nat()). hms2h({H,M,S}) -> H+(M div 60)+(S div 3600). -spec(s2hms(nat()) -> time()). s2hms(S) -> {((S div 60) div 60) rem 24, (S div 60) rem 60, S rem 60}. -spec(m2hms(nat()) -> time()). m2hms(M) -> {(M div 60) rem 24, M rem 60, 0}. -spec(h2hms(nat()) -> time()). h2hms(H) -> {H rem 24,0,0}. -spec(sub_sec(time(), nat()) -> time()). sub_sec(T,S) -> sub2(h,sub2(m,sub2(s,{T,S}))). -spec(sub_minute(time(), nat()) -> time()). sub_minute(T,M) -> sub2(h,sub2(m,{T,M})). -spec(sub_hour(time(),nat()) -> time()). sub_hour(T,H) -> sub2(h,{T,H}). -spec(add(time(),time()) -> time()). add({H,M,S},{H2,M2,S2}) -> Sp = S + S2, S3 = Sp rem 60, S4 = Sp div 60, Mp = M + M2 + S4, M3 = Mp rem 60, H3 = (H + H2 + (Mp div 60)) rem 24, {H3,M3,S3}. -spec(sub(time(),time()) -> time()). sub(T,{H,M,S}) -> {T1,M2} = sub2(s,{T,S}), {T2,H2} = sub2(m,{T1,M+M2}), sub2(h,{T2,H+H2}). %% ----------------------------------------------------------------- sub2(s,{{H,M,S},S2}) -> Ssub = S2 rem 60, {case {Ssub > S andalso M > 0, Ssub > S andalso M == 0} of {true,_} -> {H,M-1,S+60-Ssub}; {_,true} -> {H-1,M+59,S+60-Ssub}; _ -> {H,M,S-Ssub} end,(S2 - Ssub) div 60}; sub2(m,{{H,M,S},M2}) -> Msub = M2 rem 60, {case Msub > M andalso H > 0 of true -> {H-1,M+60-Msub,S}; false ->{H,M-Msub,S} end,(M2 - Msub) div 60}; sub2(h,{{H,M,S},H2}) -> {H-H2,M,S}.