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
Erlang, Testing and TDD 
Hans Törnqvist
/ November 26, 2010What about support for positive leap seconds? As an a-functional programmer (I am not really anti imio), the clock code looks like corrupt apples so I am not sure how that occasional extra second would be handled, but the test looks suspicious.
gianfrancoalongi
/ November 26, 2010Positive leap seconds? I had to google it to know what you meant 🙂 http://en.wikipedia.org/wiki/Leap_second
No, I am sorry to say that this clock lib is only defined for 24 hour systems and guarantees nothing outside of that.
Did you have anything special in mind?
Hans Törnqvist
/ November 29, 2010I did not have any hidden agenda in my first comment, but it may be worth noting in the article that some research should go into designing tests based not only on “the code”, but on real world influences as well. That is of course essential for good tests and perhaps not immediately relevant to this particular article, but pointing out pedantic details early may guide readers into spending some extra brain cycles when writing tests. Footnote? Future article? “Robust tests for interaction with the ambiguous and random behavior of some human beings”…
Or you can leave it to commentators and hope that your guests have not been damaged by the digg and youtube commentator phenomena.
gianfrancoalongi
/ November 30, 2010Well, in Erlang we adopt the “Crash often – crash early” and “Assume it is clean” approaches for (some parts of) development. This is adopted here as well, and Ergo: This library does not promise anything outside of its domain of operation. If the users wish to supply broken input data – they have nothing else to expect but broken output data.
In robust Erlang systems, it is also common to have single points of entry, where the “Ambiguous” and “Random” behaviour can entry the system. In these points it is usual to have very strict filters/logic which can handle such data. Of course such modules should be tested with such “ambiguous” and “random” behaviour in mind.
/G
Hans Törnqvist
/ December 2, 2010I agree that tests must be written according to specifications, so I am referring to problems in the specifications rather than the testing. Slightly off topic for your blag possibly 🙂 The specifications do not take into account a real world detail which may cause weird problems down the road. Who is normally responsible for writing or reviewing reliable specs?
This discussion has become rather general about TDD, perhaps we should finish this “off the record” and summarize with one last reply here for anybody interested? Who knows, this may turn into a raging flame war any second, I am a living breeding ground for those (I’ve had bad experiences online…).
gianfrancoalongi
/ December 5, 2010In “traditional” projects, there will be an architect that sets the design, from beginning to end. That person would need to think about potential problems. But assuming that the “Hard shell soft interior” view is correct, then no special consideration has to be taken for extremely weird inputs, such input should be sieved and cleaned by the Hard shell.
Cheers
/G