This is the continuation on how to to TDD with QuickCheck. Last time we had the following methods implemented and tested for the clock library.

-export([hms2s/1,hms2m/1,hms2h/1, s2hms/1,m2hms/1,h2hms/1, sub_sec/2]).

Missing are the implementations for the sub_min, and sub_hour. It’s always wise to pick the low hanging fruit first, enter sub_hour/2 test.

prop_subtract_hours_from_time() -> ?FORALL({H,M,S,H2},{nat(),nat(),nat(),nat()}, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H < 24, ?IMPLIES(H2 =< H, begin clock:sub_hour({H,M,S},H2) == {H-H2,M,S} end))))).

Needles to say, the testcode is trivial. This test will fail the preconditions many times and it is therefore wise to crank up the amount of times the test is run by using **eqc:numtests/2 ** where the first argument is an integer, the amount of tests, and the second argument is a property. The modified code becomes

prop_subtract_hours_from_time() -> eqc:numtests(500, ?FORALL({H,M,S,H2},{nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24 andalso H2 < H, ?IMPLIES(M < 60, ?IMPLIES(S < 60, begin clock:sub_hour({H,M,S},H2) == {H-H2,M,S} end))))).

I invite you to run the modified version. Now, for the slightly more complicated sub_min/2 function. While doing the test for sub_min/2, I found a bug in the old implementation, this was the error produced while running the test

zen:QCMini zenon$ make test prop_subtract_minutes_from_time: Failed! Reason: {'EXIT',{badarith,[{clock,m2hms,1}, {clock_eqc,'-prop_subtract_minutes_from_time/0-fun-0-',4}, {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,0}

The reason is that hms2m/1 produced a float value! And float values don’t work with div. So, what is needed is to either round the return value from hm2m/1 or to make it return a rounded value. As the clock library is intended to work with natural numbers, it’s best to make the functions return rounded whole values. Now, changing the hms2s/1, hms2m/1 and hms2h/1 functions will require changing the tests. Which is kind of the point of having the tests in the first place. Changing the implementation should alert the programmer that the behaviour has changed. Now the test looks like

prop_subtract_minutes_from_time() -> ?FORALL({H,M,S,M2},{nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(M2 =< ((H*60)+M), begin T = {H,M,S}, clock:sub_minute(T,M2) == clock:m2hms((clock:hms2m(T) - M2)) end))))).

The test continues to fail

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

This time due to the fact that the model in the QuickCheck test will round the Right Hand Side (RHS) and calculate the LHS without rounding! Clearly, we can’t use the m2hms/1 for this test. The solution is to go by the smallest possible unit, the second.

clock:sub_minute(T,M2) == clock:s2hms((clock:hms2s(T) - (M2*60)))

And voila!

zen:QCMini zenon$ make test prop_subtract_minutes_from_time: .......x..xx.x...............x...x...... .....................................x.......xx.............x....... x.xx. OK, passed 100 tests

Of course I made proper changes to the other tests in order to keep all functions to returning whole integer values (not using round!) [left as an exercise].

Now it is left to write a test for the add/2 function, the add function will allow us to add two time() values together, wrapping on 24, so the added value is in the bounds of time() as well.

*Due to the intended cyclic behaviour on 24, we will have to make adjustments to the other functions first. Making sure everything is working within the bounds of the 24 hour system (00:00:00 – 23:59:59). This minor modification just means adding some (rem 24) to the _2hms/1 functions and changing some tests. Do this first.*

Now the test

prop_add_time() -> ?FORALL({H,M,S,H2,M2,S2},{nat(),nat(),nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H2 < 24, ?IMPLIES(M2 < 60, ?IMPLIES(S2 < 60, 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))))))).

And the proof that the implementation

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

is working

zen:QCMini zenon$ make test prop_add_time: ...................................................... ........................x.............x.x.xx..xxx.xxxxxxx.xx.x.x. OK, passed 100 tests

Great! Last API function left, sub/2, it will be somewhat similar to the sub_sec/2, but the test first of all

prop_sub_time() -> ?FORALL({H,M,S,H2,M2,S2},{nat(),nat(),nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H2 < 24, ?IMPLIES(M2 < 60, ?IMPLIES(S2 < 60, ?IMPLIES(((H*3600) + M*60 + S) >= ((H2*3600) + M2*60 + S2), begin T = {H,M,S}, T2= {H2,M2,S2}, {HRes,MRes,SRes} = clock:sub(T,T2), HRes >= 0 andalso MRes >= 0 andalso SRes >= 0 andalso {HRes,MRes,SRes} == clock:s2hms(clock:hms2s(T) - clock:hms2s(T2)) end))))))))

Do not fret that this is ugly, the next post on this topic will show you how to fix this up in a good way.

sub({H,M,S},{H2,M2,S2}) -> Sres = S - (S2 rem 60), Mres = M - (S2 div 60) - M2, Hres = H - (M div 60) - H2, 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 voila, running the tests for 100 (or like I did 1000) runs makes it pass

zen:QCMini zenon$ make test prop_sub_time: ....x...x.x..xx.xx...xxxx.x..x.x..x..x..x.xx.x.xx..x..xx.x. .x......x.xx.xx.xx...x.x..xxx.xx...x.xx.x..x.xx..xxxxxx.xxxx...xx....xx.. xx.xxxxxx.x...xxx.xxx.xx.xx..xxx..xxxx.x.xxxxxxxxxxxxxxxx.x.xxxxx. (removed lines) OK, passed 10000 tests

End of this story! We now have the clock lib for working with time() values. Now follows the full code. And next time we will start refactoring and tidying up the clock lib, also the testfile, and write our own generators to make the clock_eqc.erl look better.

## The implementation module (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({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. -spec(sub_hour(time(),nat()) -> time()). sub_hour({H,M,S},H2) -> {H-H2,M,S}. -spec(sub_minute(time(), nat()) -> time()). sub_minute({H,M,S},M2) -> case M2 > M of true -> {H-1,(M+60)-M2,S}; false -> {H,M-M2,S} end. -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({H,M,S},{H2,M2,S2}) -> Sres = S - (S2 rem 60), Mres = M - (S2 div 60) - M2, Hres = H - (M div 60) - H2, 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.

## The test module (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). 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)))). 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 div 60)))). 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 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({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))))). prop_subtract_hours_from_time() -> eqc:numtests(100, ?FORALL({H,M,S,H2},{nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24 andalso H2 < H, ?IMPLIES(M < 60, ?IMPLIES(S < 60, begin clock:sub_hour({H,M,S},H2) == {H-H2,M,S} end))))). prop_subtract_minutes_from_time() -> ?FORALL({H,M,S,M2},{nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(M2 =< ((H*60)+M), begin T = {H,M,S}, clock:sub_minute(T,M2) == clock:s2hms((clock:hms2s(T) - (M2*60))) end))))). prop_add_time() -> ?FORALL({H,M,S,H2,M2,S2},{nat(),nat(),nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H2 < 24, ?IMPLIES(M2 < 60, ?IMPLIES(S2 < 60, 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() -> eqc:numtests(1000, ?FORALL({H,M,S,H2,M2,S2},{nat(),nat(),nat(),nat(),nat(),nat()}, ?IMPLIES(H < 24, ?IMPLIES(M < 60, ?IMPLIES(S < 60, ?IMPLIES(H2 < 24, ?IMPLIES(M2 < 60, ?IMPLIES(S2 < 60, ?IMPLIES(((H*3600) + M*60 + S) >= ((H2*3600) + M2*60 + S2), begin T = {H,M,S}, T2= {H2,M2,S2}, {HRes,MRes,SRes} = clock:sub(T,T2), HRes >= 0 andalso MRes >= 0 andalso SRes >= 0 andalso {HRes,MRes,SRes} == clock:s2hms(clock:hms2s(T) - clock:hms2s(T2)) end))))))))).

## Next time

Cleaning up and refactoring of the modules. Generators for our cases and extra material on quickcheck.

Cheers

/G