Automated Testing – Bringing out the big guns – Part 3


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

Automated Testing – Bringing out the big guns – Part 2


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

Automated Testing – Bringing out the big guns – Part 1


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)

  1. A module including the quickcheck application header file, 

    -include_lib(“eqc/include/eqc.hrl”).

  2. Inside the same module, properties you will run your test on, each property must be exported.
  3. 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 collecting 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

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: