plspec_test.pl

atom_member(X, [X|_]) :- !.

atom_member(X, [_|T]) :-
    atom_member(X, T).

bar(A) :-
    my_tuple_with_incorrect_spec(A).

bind_to_zero(0).

foo(A,B) :-
    my_member(A,B).

if_atom_then_my_atomic(X) :-
    (atom(X) -> my_atomic(X)).

if_my_atomic_then_atom(X) :-
    (my_atomic(X) -> atom(X)).

int(even, X) :- 0 is X mod 2.

int(odd, X) :- 1 is X mod 2.

invariant_violator(X) :-
    X = [1], X == [2]. % fail in a more sophisticated way

invariant_violator(a).

my_and_test(_).

my_atomic([_|_]) :- !, fail.

my_atomic(_).

my_compound_foo(foo(_)).

my_member(E,[E|_]).

my_member(E,[_|T]) :-
    my_member(E,T).

my_or_test(_).

my_tuple_with_incorrect_spec([X, X]).

not_my_atomic(X) :-
    \+ my_atomic(X).

partial_instantiator([_,_]).

partial_instantiator([1,_]).

partial_instantiator([_,2]).

partial_instantiator([_,a]).

test(conform_call1) :-
    my_compound_foo(foo(1)).

test(conform_call2) :-
    my_compound_foo(foo(bar)).

test(conform) :-
    my_tuple_with_incorrect_spec([a, a]).

test(conform) :-
    my_atomic([]).

test(conform2) :-
    \+ my_atomic([foo]).

test(conform3) :-
    my_atomic(foo).

test(conform4) :-
    my_atomic(2).

test(conform) :-
    my_or_test(foo).

test(conform) :-
    my_and_test(foo).

test(conform) :-
    invariant_violator(a).

test(conform2) :-
    \+ invariant_violator(b).

test(empty_is_tree) :-
    valid(tree(int), empty).

test(tree1) :-
    valid(tree(int), node(empty, 1, empty)).

test(tree2) :-
    valid(tree(int), node(node(empty, 1, empty),
    2,
    node(empty, 3, empty))).

test(tree3) :-
    \+ valid(tree(int), node(node(empty, 1, empty),
    a,
    node(empty, 3, empty))).

test(tree3) :-
    \+ valid(tree(int), node(node(empty, 1, emppty),
    1,
    node(empty, 3, empty))).

test(zero_is_even) :-
    valid(int(even), 0).

test(zero_is_not_odd) :-
    \+ valid(int(odd), 0).

test(one_is_odd) :-
    valid(int(odd), 1).

test(one_is_not_even) :-
    \+ valid(int(even), 1).

test(instantiated_call, [nondet]) :-
    my_member(a, [a, b, c]).

test(partly_instantiated, [nondet]) :-
    my_member(_, [a, b, c]).

test(partly_instantiated_not_conform, [nondet, throws(_)]) :-
    % second argument is not a list
    my_member(a, _).

test(partly_instantiated3, [nondet]) :-
    my_member(c, [a, _, c]).

test(all_variables_not_conform, [nondet, throws(_)]) :-
    my_member(_, _).

test(not_conform, [throws(_)]) :-
    my_member([], a).

test(nonconform_call, [throws(_)]) :-
    my_compound_foo(foo(_)).

test(not_conform, [throws(_)]) :-
    my_compound_foo(bar(_)).

test(conform_var, [throws(_)]) :-
    my_tuple_with_incorrect_spec([a, _]).

test(conform_var2, [throws(_)]) :-
    my_tuple_with_incorrect_spec([_, a]).

test(nonconform_both_var, [throws(_)]) :-
    my_tuple_with_incorrect_spec([_, _]).

test(conform, [nondet]) :-
    atom_member(a, [a,b,c]).

test(not_conform, [throws(_)]) :-
    atom_member(a, X), !,
    X = [a,b,c].

test(not_conform2, [throws(_)]) :-
    atom_member(a, [a,_|_]).

test(not_conform3, [throws(_)]) :-
    atom_member(a, [1,_|_]).

test(not_conform1, [throws(_)]) :-
    my_atomic(foo(_)).

test(not_conform2, [throws(_)]) :-
    \+ my_atomic([_]).

test(not_conform3, [throws(_)]) :-
    my_atomic([[2]]).

test(not_conform4, [throws(_)]) :-
    \+ my_atomic([_]).

test(nonconform, [throws(_)]) :-
    my_or_test(_).

test(nonconform, [throws(_)]) :-
    my_and_test([1]).

test(nonconform2, [throws(_)]) :-
    my_and_test(_).

test(nonconform, [throws(_)]) :-
    invariant_violator(_).

test(conform, [nondet]) :-
    partial_instantiator([_,_]).

test(conform2, [nondet]) :-
    partial_instantiator([X, _]), X == 1.

test(conform3, [nondet]) :-
    partial_instantiator([_, 2]).

test(conform4, [nondet]) :-
    partial_instantiator([1, 2]).

test(nonconform, [throws(_)]) :-
    partial_instantiator([a, 2]).

test(nonconform2, [throws(_)]) :-
    findall(A, partial_instantiator(A), _).

test(postcondition_violated, [throws(_)]) :-
    bind_to_zero(_).