Examples (unittest)

Stability: [beta] Most of the functionality is there but it is still missing some testing and/or verification.

Some examples of the use of test assertions.

:- module(test_examples,
    [
        p/1,
        display1/1,
        call_test10/1,
        cut_test5/0,
        display_fail/0
    ],
    [assertions, nativeprops, basicmodes, rtchecks, unittestdecls, hiord]).

:- doc(author, "Edison Mera").
:- doc(author, "Nataliia Stulova").

:- doc(module, "Some examples of unit tests.").

:- use_module(engine(io_basic)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% ----------------------------------------------------------------------
% tests only with preconditions

:- test p(A) : (A = c) %+ (possible_exceptions([_]))
    # "test should pass".
:- test p(A) : (A = d, A = a)
    # "test should fail (precondition)".
:- test p(A) : (A = exception, throw(A))
    # "test should fail (throws exception in precondition)".
:- test p(A) : (A = h)
    # "test should abort".

% ----------------------------------------------------------------------
% tests with preconditions and computational properties

:- test p(A) : (A = a) + not_fails
    # "test should pass".
:- test p(A) : (A = b) + fails
    # "test should pass".
:- test p(A) : (A = c) + exception(error(c, _))
    # "test should pass".
:- test p(A) : (A = c) + (fails, no_exception)
    # "test should fail".
:- test p(A) : (A = c) + not_fails
    # "test should fail".

% ----------------------------------------------------------------------
% tests with preconditions and postonditions

:- test p(Z) => (Z = d).

% ----------------------------------------------------------------------
% assertions that can be added to all unit tests for p/1 with the
% 'rtc_entry' unittest option
:- check comp p(X) : (X = a) + not_fails.
% :- check comp p(X) : (X = b) + not_fails.

p(a).                               % rule succeeds
p(b) :- fail.                       % rule fails
p(c) :- throw(error(c, 'error c')). % rule throws an exception
p(h) :- halt(1).                    % rule aborts the execution (note: cannot be used with 'sameproc' option)

% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% ----------------------------------------------------------------------
% this set of tests demonstrates the correct and incorrect uses of texec
% assertions, it only gives examples of passing tests
%
:- texec display1(A) : (A = hello)
    # "correct texecassertion, test should pass".
:- texec display1(A) : (A = hello) + user_output("hello")
    # "incorrect texec assertion, test should pass".
% ----------------------------------------------------------------------

% ----------------------------------------------------------------------
% examples of the alternatives for the texec assertions above
%
:- test display1(A) : (A = hello)
    # "test should pass".
:- test display1(A) : (A = hello) + user_output("bye")
    # "test should fail".
% ----------------------------------------------------------------------

display1(A) :- display(A).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- test display_fail + (user_output("hello"), fails) # "Test OK".

display_fail :- display(hello), fail.

:- pred display_fail(A) + (user_output("hello2"), fails).
:- export(display_fail/1).

display_fail(_A) :- display(hello), fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- use_module(library(write), [write/1]).

:- test cut_test5 + (user_output("Cut disjunction"), fails) #
    "Test OK".

cut_test5 :- (! ; write('No')), write('Cut disjunction'), fail.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- test call_test10(X) : (X=(write(3), call(1)))
    + ( user_output("output"),
        exception(error(type_error(callable, 1), 'in metacall')) )
# "Wrong test".

:- meta_predicate call_test10(goal).

call_test10(X) :- call(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- export(qs/2).
:- pred qs(+list(int), -list(int)) + is_det.

qs(A, A).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% tests below cover most of scenarios of the unit test expansion
%% (missing: tests that take into account different values of prolog flags
%%  rtchecks_predloc and rtchecks_asrloc (see rtchecks_tr:combine_locators/6)
%%  for the reason behind).

%% tests for different uses of GP properties in texec assertions

:- use_module(library(unittest/unittest_props), [try_sols/2]).

:- export(case_tx/2).

% processing texec as texec

:- texec case_tx(A, AB) : (A = a)
     # "test should pass".
:- texec case_tx(A, AB) : (A = a) + try_sols(2)
     # "test should pass".

% processing texec as test

:- texec case_tx(A, AB) : (A = a) + is_det
     # "test should fail, bug: true&false test".
:- texec case_tx(A, AB) : (A = a) + (try_sols(2), non_det)
     # "test should pass".

case_tx(a, a).
case_tx(a, b).

% ----------------------------------------------------------------------

%% tests for different uses of AP and GP properties in test assertions

:- export(case_ts/2).

:- test case_ts(X, Y) : (X = a)
    # "test should pass".
:- test case_ts(X, Y) : (X = a) + try_sols(1)
    # "test should pass".
:- test case_ts(X, Y) : (X = b) + is_det
    # "test should pass".
:- test case_ts(X, Y) : (X = a) => (Y = b) + try_sols(1)
    # "test should fail".
:- test case_ts(X, Y) : (X = b) => (Y = a ; Y = b) + is_det
    # "test should pass".

% ----------------------------------------------------------------------

%% checks for the properties in the assertions are added to the unit
%% tests for case_ts/2 iff this module does not include the rtchecks
%% package. To see the effects of this assertions remove the rtchecks
%% package from the package list and run the tests for this module
%% wuth the [rtc_entry] test option. If you do not remove the
%% package, the assertions below will be simply turned into rtchecks.

% :- pred case_ts(X,Y) : atm(X) => int(Y) # "makes unit tests fail".
% :- pred case_ts(X,Y) : atm(X) => gnd(Y) # "does not affect unit tests".

case_ts(a, a).
case_ts(a, b).
case_ts(b, b).

:- module(ceval1, [ceval/2], [assertions, regtypes, nativeprops]).

:- doc(author, "Edison Mera").

:- doc(module, "This example illustrates how the unified approach for
   static verification, run-time checking, and unit testing works. It
   captures the situation in which the programmer changes the main
   functor of a data structure. In this case, the regular type complex
   c(A, B) is renamed to cm(A, B).  This file contains the initial
   program.").

:- entry ceval/2 : gnd * var.

:- regtype complex/1.
:- export(complex/1).

complex(c(A, B)) :-
    num(A),
    num(B).

:- test ceval(A, B) : (A = c(3, 4) + c(1, 2) - c(2, 3))
    => (B = c(2, 3)) + (not_fails, is_det).

:- test ceval(A, B) : (A = c(3, 4) * c(1, 2) / c(1, 2))
    => (B = c(3.0, 4.0)) + (not_fails, is_det).

:- check pred ceval/2 : gnd * term => gnd * complex.

ceval(A,   A) :- complex(A), !.
ceval(A+B, C) :- ceval(A, CA), ceval(B, CB), add(CA, CB, C).
ceval(A-B, C) :- ceval(A, CA), ceval(B, CB), sub(CA, CB, C).
ceval(A*B, C) :- ceval(A, CA), ceval(B, CB), mul(CA, CB, C).
ceval(A/B, C) :- ceval(A, CA), ceval(B, CB), div(CA, CB, C).

:- pred add/3 : complex * complex * var => complex * complex * complex.
add(c(A1, B1), c(A2, B2), c(A, B)) :-
    A is A1 + A2,
    B is B1 + B2.

:- pred sub/3 : complex * complex * var => complex * complex * complex.
sub(c(A1, B1), c(A2, B2), c(A, B)) :-
    A is A1 - A2,
    B is B1 - B2.

:- pred mul/3 : complex * complex * var => complex * complex * complex.
mul(c(A1, B1), c(A2, B2), c(A, B)) :-
    A is A1*A2 - B1*B2,
    B is A1*B2 + B1*A2.

:- pred div/3 : complex * complex * var => complex * complex * complex.
div(c(A1, B1), c(A2, B2), c(A, B)) :-
    D is A2*A2 + B2*B2,
    A is (A1*A2 + B1*B2) / D,
    B is (A2*B1 - A1*B2) / D.

:- module(ceval2, [ceval/2], [assertions, regtypes, nativeprops]).

:- doc(author, "Edison Mera").

:- doc(module, "This example illustrates how the unified approach for
   static verification, run-time checking, and unit testing works. It
   captures the situation in which the programmer changes the main
   functor of a data structure. In this case, the regular type complex
   c(A, B) is renamed to cm(A, B).  This file contains the renamed
   program (with a bug).").

:- entry ceval/2 : gnd * var.

:- regtype complex/1.
:- export(complex/1).

complex(cm(A, B)) :-
    num(A),
    num(B).

:- false test ceval(A, B) : (A = cm(3, 4) + cm(1, 2) - cm(2, 3))
    => (B = cm(2, 3)) + (not_fails, is_det).

:- test ceval(A, B) : (A = cm(3, 4) * cm(1, 2) / cm(1, 2))
    => (B = cm(3.0, 4.0)).

:- check pred ceval/2 : gnd * term => gnd * complex.

ceval(A,   A) :- complex(A), !.
ceval(A+B, C) :- ceval(A, CA), ceval(B, CB), add(CA, CB, C).
ceval(A-B, C) :- ceval(A, CA), ceval(B, CB), sub(CA, CB, C).
ceval(A*B, C) :- ceval(A, CA), ceval(B, CB), mul(CA, CB, C).
ceval(A/B, C) :- ceval(A, CA), ceval(B, CB), div(CA, CB, C).

:- pred add/3 : complex * complex * var => complex * complex * complex.
add(cm(A1, B1), cm(A2, B2), cm(A, B)) :-
    A is A1 + A2,
    B is B1 + B2.

:- pred sub/3 : complex * complex * var => complex * complex * complex.
sub(cm(A1, B1), cm(A2, B2), c(A, B)) :- % You forgot to rename c to cm!
    A is A1 - A2,
    B is B1 - B2.

:- pred mul/3 : complex * complex * var => complex * complex * complex.
mul(cm(A1, B1), cm(A2, B2), cm(A, B)) :-
    A is A1*A2 - B1*B2,
    B is A1*B2 + B1*A2.

:- pred div/3 : complex * complex * var => complex * complex * complex.
div(cm(A1, B1), cm(A2, B2), cm(A, B)) :-
    D is A2*A2 + B2*B2,
    A is (A1*A2 + B1*B2) / D,
    B is (A2*B1 - A1*B2) / D.

:- module(length, [length/2, concat/3],
        [assertions, isomodes, metatypes, hiord, nativeprops]).

:- doc(author, "Alvaro Sevilla San Mateo").

length([],    0).
length([_|T], N) :- length(T, N0), N is N0 + 1.

concat([],     L,  L).
concat([X|L1], L2, [X|L3]) :- concat(L1, L2, L3).

:- test length(X, Y) : (X = [1, 2, 3], Y = 3) + not_fails.
:- test length(X, Y) : (X = [a, b, c, d, e], Y = 5) + not_fails.
:- test length(X, Y) : (X = [], Y = 0) + not_fails.
:- test length(X, Y) : (X = [a, b, c, d, e], Y = 5) + not_fails.
:- test length(X, Y) : (X = [a, b, c], Y = 5) + fails.
:- test length(X, Y) : (X = [a, b, c, d], Y = 5) + fails.
:- test concat(A, B, C) : (A = [1, 2], B = [3], C = [1, 2, 3]) + not_fails.
:- test concat(A, B, C) : (A = [1, 2], B = [3], var(C)) => (C=[1, 2, 3])
    + not_fails.

:- module(civil_registry, [profession/1, surname/1, sevillian/1,
            family_income/1, married/2, salary/2],
        [assertions, isomodes, metatypes, hiord, nativeprops]).

:- doc(author, "Alvaro Sevilla San Mateo").

family_information(husband(name(antonio, garcia, fernandez),
            profession(architect), salary(300000)),
        wife(name(ana, ruiz, lopez),
            profession(teacher), salary(120000)),
        address(sevilla)).

family_information(husband(name(luis, alvarez, garcia),
            profession(architect), salary(400000)),
        wife(name(ana, romero, soler),
            profession(housewife), salary(0)),
        address(sevilla)).

family_information(husband(name(bernardo, bueno, martinez),
            profession(teacher), salary(120000)),
        wife(name(laura, rodriguez, millan),
            profession(doctor), salary(250000)),
        address(cuenca)).


family_information(husband(name(miguel, gonzalez, ruiz),
            profession(businessman), salary(400000)),
        wife(name(belen, salguero, cuevas),
            profession(housewife), salary(0)),
        address(dos_hermanas)).

profession(X) :- family_information(husband(_,profession(X),_),_,_).
profession(X) :- family_information(_,wife(_,profession(X),_),_).

:- test profession(X) : (X = doctor) + not_fails.
:- test profession(X) : (X = businessman) + not_fails.
:- test profession(X) : (X = computer_scientist) + fails.

surname(X) :-
    family_information(husband(name(_, X, _), _, _), _, _).
surname(X) :-
    family_information(_, wife(name(_, X, _), _, _), _).

:- test surname(X) : (X = alvarez) + not_fails.
:- test surname(X) : (X = salguero) + not_fails.
:- test surname(X) : (X = sanchez) + fails.

sevillian(X) :-
    family_information(husband(X, _, _), _, address(sevilla)).
sevillian(X) :-
    family_information(_, wife(X, _, _), address(sevilla)).

:- test sevillian(X) : (X = name(miguel, gonzalez, ruiz)) + fails.
:- test sevillian(X) : (X = name(belen, salguero, cuevas)) + fails.
:- test sevillian(X) : (X = name(pedro, sanchez, rodriguez)) + fails.
:- test sevillian(X) : (X = name(antonio, garcia, fernandez)) + not_fails.

family_income(X) :-
    family_information(
        husband(_, _, salary(N1)),
        wife(_, _, salary(N2)), _),
    X is N1+N2.

:- test family_income(X) : (X = 400000) + not_fails.
:- test family_income(X) : (X = 370000) + not_fails.
:- test family_income(X) : (X = 100) + fails.

married(X, Y) :-
    family_information(
        husband(name(X, _, _), _, _),
        wife(name(Y, _, _), _, _), _).

:- test married(X, Y) : (X = antonio, Y = ana) + not_fails.
:- test married(X, Y) : (X = miguel, Y = belen) + not_fails.
:- test married(X, Y) : (X = antonio, Y = maria) + fails.

salary(X, Y) :-
    family_information(husband(X, _, salary(Y)), _, _).
salary(X, Y) :-
    family_information(_, wife(X, _, salary(Y)), _).

:- test salary(X, Y) : (X = name(luis, alvarez, garcia), Y = 400000)
    + not_fails.
:- test salary(X, Y) : (X = name(laura, rodriguez, millan), Y = 250000)
    + not_fails.
:- test salary(X, Y) : (X = ana, Y = 100) + fails.

:- module(_, [qsort/2], [assertions, nativeprops]).

:- doc(author, "Edison Mera").

:- doc(module, "This example illustrates how the unified approach
    for static verification, run-time checking and unit testing
    works. In this case, a bug have been introduced: in the call
    to append/3 by qsort/2, variables R1 and R2 are swapped.  Then
    we prove statically part of the assertions, for the part that
    cannot be verified statically we generate run-time checks,
    and finally, the program also has a test attached that
    exercises the run-time checks.").

:- prop sorted_num_list/1.
:- export(sorted_num_list/1).

sorted_num_list([]).
sorted_num_list([X]) :- number(X).
sorted_num_list([X, Y|Z]) :-
    number(X), number(Y), X<Y, sorted_num_list([Y|Z]).

:- calls partition(A, B, C, D) : (ground(A), ground(B)).
:- comp partition(A, B, C, D) : (list(num, A)) + (not_fails, is_det).
:- success partition(A, B, C, D) => (ground(C), list(num, D)).

partition([],    _B, [],        []).
partition([E|R], C,  [E|Left1], Right) :-
    E < C, !, partition(R, C, Left1, Right).
partition([E|R], C, Left, [E|Right1]) :-
    E >= C, partition(R, C, Left, Right1).

:- calls append(A, B, C) : (list(num, A), list(num, B)).

append([],    X, X).
append([H|X], Y, [H|Z]) :- append(X, Y, Z).

:- entry qsort(A, B) : (list(num, A), ground(A)).

:- test qsort(A, B) : (A = [5, 7, 2, 4, 3]) => (B = [2, 3, 4, 5, 7]).

:- calls qsort(A, B) : list(num, A).
:- comp qsort(A, B) : (list(num, A), ground(A), var(B)) + is_det.
:- success qsort(A, B) => (ground(B), sorted_num_list(B)).

qsort([X|L], R) :-
    partition(L, X, L1, L2),
    qsort(L2, R2), qsort(L1, R1),
    append(R2, [X|R1], R). % There is a bug here!!!
qsort([], []).

:- module(relationships,
        [father/2, son/2, grandfather/2, brother/2, fsb/2],
        [assertions, isomodes, metatypes, hiord, nativeprops]).

:- doc(author, "Alvaro Sevilla San Mateo").

father('juan',   'maria'). % juan is the father of maria
father('pablo',  'juan').  % pablo is the father of juan
father('pablo',  'marcela').
father('carlos', 'debora').

% A is the son of B if B the father of A
son(A, B) :- father(B, A).

% A is the grandfather of B if A is the father of C and C is the father of B 
grandfather(A, B) :-
    father(A, C),
    father(C, B).

% A and B are brothers if the father of A is also the father of B and A and B are different persons
brother(A, B) :-
    father(C, A),
    father(C, B),
    A \== B.


% A and B are fsb if A is the father, son, or brother of B
fsb(A, B) :-
    father(A, B).
fsb(A, B) :-
    son(A, B).
fsb(A, B) :-
    brother(A, B).

% Tests
:- test fsb(A, B) : (A = 'juan', B = 'marcela') + not_fails.
:- test fsb(A, B) : (A = 'pedro', B = 'pedro') + not_fails.
:- test fsb(A, B) : (A = 'debora', B = 'carlos') + fails.
:- test fsb(A, B) : (A = 'debora', B = 'nadie') + not_fails.
:- test brother(A, B) : (A = 'debora', B = 'carlos') + not_fails.