Examples of types, modes, and resources in CiaoPP

A first example - no assertions

Consider the classic implementation of quick-sort:

%! \begin{code}
:- module(_,[qsort/2],[assertions,nativeprops,modes]).

% With no information on the calls to qsort/2, 
% the analyzer warns that it cannot ensure that 
% the calls to =</2 and >/2 will not generate a 
% run-time error.

qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X =< F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X > F,
    partition(Y,F,Y1,Y2).

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
V,assertion=[assertion],filter=warn_error
%! \end{opts}

If no other information is provided, the exported predicate qsort/2 can be called with arbitrarily instantiated terms as arguments (e.g., with a list of variables). This implies that the library predicates =</2 and >/2 in partition/4 can also be called with arbitrary terms and thus run-time errors are possible, since =</2 and >/2 require their arguments to be bound to arithmetic expressions when called. Even though there are no assertions in the program itself, the system is able to warn that it cannot verify that the calls to =</2 and >/2 will not generate a run-time error (by clicking the question mark (?) in the right top corner, you can run CiaoPP and see the messages). This is the result of a modular global analysis and a comparison of the information inferred for the program points before the calls to =</2 and >/2 with the assertions that express the calling restrictions for =</2 and >/2. Such assertions live in the libraries that provide these standard predicates. Further details can be obtained by reading the messages.

Adding an assertion

We can add an assertion for the exported predicate qsort/2 expressing that it should be called with its first argument bound to a list of numbers:

%! \begin{code}
:- module(_,[qsort/2],[assertions,nativeprops,modes]).

% Adding information on how the exported predicate should 
% be called the system can infer that =</2 and >/2 will be 
% called correctly, and no warnings are flagged.

:- pred qsort(+list(num),_).

qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X =< F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X > F,
    partition(Y,F,Y1,Y2).

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
V,assertion=[assertion],filter=all_message
%! \end{opts}

Assuming this ''entry'' information, the Ciao system can verify that all the calls to =</2 and >/2 are now correct (with their arguments bound to numbers in this case), and thus no warnings are displayed. Note that in practice this assertion may not be necessary since this information could be obtained from the analysis of the caller(s) to this module.

Adding more assertions

Let us now add more assertions to the program, stating properties that we want checked:

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

% qsort/2 with some assertions.
% The system verifies the assertions and also that 
% the =</2 and >/2 are called correctly and will not 
% generate any run-time errors.  
% Try also generating the documentation for this file!

% If qsort/2 is called with a list of numbers, it will
% return a list of numbers and at most one solution.
:- pred qsort(+list(num),-list(num)) + semidet.
 
qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

% partition/4 is called with a list of numbers and a
% number it returns two lists of numbers, one solution,
% and will never fail. 
:- pred partition(+list(num),+num,-list(num),-list(num)) + det.

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X =< F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X > F,
    partition(Y,F,Y1,Y2).

% append/3 is called with two lists of numbers, will
% return a list of numbers, and at most one solution.
:- pred append(+list(num),+list(num),-list(num)) + semidet.

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).

For example, the assertion for predicate partition/4 (line 23):

:- pred partition(+list(num),+num,-list(num),-list(num)) + det.

expresses, using modes, that the first argument should be bound to a list of numbers, and the second to a number, and that, for any terminating call meeting this call pattern: a) if the call succeeds, then the third and fourth arguments will be bound to lists of numbers; and b) the call is deterministic, i.e., it will produce one solution exactly, property det in the + field, which is inferred in CiaoPP as the conjunction of two properties: 1) the call does not (finitely) fail (property not_fails) and 2) the call will produce one solution at most (property is_det). Similarly, the assertion for qsort/2:

:- pred qsort(+list(num),-list(num)) + semidet.

expresses the expected calling pattern, and that the call can have at most one answer, property semidet.

All the assertions in the program indeed get verified by CiaoPP, which is shown in the output:

:- checked calls qsort(_A,_B)
   : list(num,_A).

:- checked success qsort(_A,_B)
   : list(num,_A)
   => list(num,_B).

:- checked comp qsort(_A,_B)
   : list(num,_A)
   + semidet.

:- checked calls partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) ).

:- checked success partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) )
   => ( list(num,_C), list(num,_D) ).

:- checked comp partition(_A,_B,_C,_D)
   : ( list(num,_A), num(_B) )
   + det.

:- checked calls append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) ).

:- checked success append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) )
   => list(num,_C).

:- checked comp append(_A,_B,_C)
   : ( list(num,_A), list(num,_B) )
   + semidet.

Modes in the Ciao assertion model

In the Ciao assertion model, modes are macros that serve as a shorthand for assertions, in particular predicate-level assertions. These are in general of the form:

:- [Status] pred Head : Pre => Post + Comp.

where Head denotes the predicate that the assertion applies to, and Pre and Post are conjunctions of state property literals. Pre expresses properties that hold when Head is called. Post states properties that hold if Head is called in a state compatible with Pre and the call succeeds. Comp describes properties of the whole computation such as determinism, non-failure, resource usage, termination, etc., also for calls that meet Pre. In particular, thanks to the modes package included in the module declaration in the previous example:

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

the modes used for qsort/2:

:- pred qsort(+list(num),-list(num)) + semidet.

are expanded to the assertion:

:- pred qsort(X,Y) : list(num,X) => list(num,Y) + semidet.

Using the doccomments package

In this example the assertions are written as machine readable comments enabled by the doccomments package. Such comments can contain embedded assertions, which are also verified. Here we use again modes and determinacy. This format is familiar to Prolog programmers and compatible with any Prolog system without having to define any operators for the assertion syntax. If we run the example, we can see that, as before, the assertions get verified by CiaoPP:

%! \begin{code}
:- module(_,[qsort/2],[assertions,nativeprops,regtypes,modes,doccomments]).

% Describing predicates with modes/assertions in doccommmments syntax
% (which also get verified by the system). Try also generating the 
% documentation for this file!

%! qsort(+list(num),-list(num)): 
%  Y is X sorted.
qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

%! partition(+list(num),+num,-list(num),-list(num)): 
%  Partitions a list into two lists, greater and
%  smaller than second argument. 
partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X =< F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X > F,
    partition(Y,F,Y1,Y2).

%! append(+list(num),+list(num),-list(num)): 
append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
V,ana_det=nfdet,output=on,filter=check_pred
%! \end{opts}

Detecting possible failure

Imagine that we replace =</2 with </2 in the second clause of partition/4,

%! \begin{code}
:- module(_,[qsort/2],[assertions,nativeprops,regtypes,modes]).

% qsort/2 with some assertions.
% If we have </2 and >/2 in partition the system warns 
% that partition/4 is not guaranteed to not fail.

:- pred qsort(+list(num),-list(num)) + semidet.
 
qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

:- pred partition(+list(num),+num,-list(num),-list(num)) + det.

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X < F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X > F,
    partition(Y,F,Y1,Y2).

:- pred append(+list(num),+list(num),-list(num)) + semidet.

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
V,ana_det=nfdet,filter=warn_error
%! \end{opts}

CiaoPP warns that this predicate may fail. This is because the case where X=F is not ''covered'' by the ''tests'' of partition/4.

Detecting possible non-determinism

Conversely, if we replace >/2 with >=/2 in the second clause of the original definition of partition/4,

%! \begin{code}
:- module(_,[qsort/2],[assertions,nativeprops,regtypes,modes]).

% qsort/2 with some assertions.
% If we have =</2 and >=/2 in partition the system warns 
% that both partition/4 and qsort/2 may not be deterministic.

:- pred qsort(+list(num),-list(num)) + semidet.
 
qsort([], []).
qsort([First|Rest],Result) :-
    partition(Rest,First,Sm,Lg), 
    qsort(Sm,SmS), 
    qsort(Lg,LgS),
    append(SmS,[First|LgS],Result).

:- pred partition(+list(num),+num,-list(num),-list(num)) + det.

partition([],_,[],[]).
partition([X|Y],F,[X|Y1],Y2) :- 
    X =< F, 
    partition(Y,F,Y1,Y2).
partition([X|Y],F,Y1,[X|Y2]) :- 
    X >= F,
    partition(Y,F,Y1,Y2).

:- pred append(+list(num),+list(num),-list(num)) + semidet.

append([],Xs,Xs).
append([X|Xs],Ys,[X|Zs]) :-
    append(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
V,ana_det=nfdet,filter=warn_error
%! \end{opts}

the system warns that the predicate may not be deterministic. This is because the analyzer infers that not all the clauses of partition/4 are pairwise mutually exclusive (in particular the second and third clauses are not), and thus, multiple solutions may be obtained.

Defining properties

The reader may be wondering at this point where the properties that are used in assertions (such as list(num)) come from. As mentioned before, such properties are typically written in Prolog and its extensions; and they can also be built-in and/or defined and imported from system libraries or in user code. Visibility is controlled by the module system as for any other predicate.

%! \begin{focus}
:- module(_,[color/1,colorlist/1,sorted/1],[assertions,regtypes,clpq]).

% Defining some types and properties which can then be used 
% in assertions.

:- regtype color/1.
color(red).
color(green).
color(blue).

:- regtype colorlist/1.
colorlist([]).
colorlist([H|T]) :- color(H), colorlist(T).

:- prop sorted/1.
sorted([]).
sorted([_]).
sorted([X,Y|T]) :- X .>=. Y, sorted([Y|T]).
%! \end{focus}

The above example shows some examples of definitions of properties. Two of them are marked as regular types (regtype directive): color/1, defined as the set of values {red, green, blue}, and colorlist/1, representing the infinite set of lists whose elements are of color type. The third property is not a regular type, but an arbitrary property (prop directive), representing the infinite set of lists of numeric elements in descending order. Marking predicates as properties allows them to be used in assertions, but they remain regular predicates, and can be called as any other, and also used as run-time tests, to generate examples (test cases), etc. For example:

?- colorlist(X).

or, we can select breadth-first execution (useful here for fair generation) by adding the package sr/bffall.

:- module(_,[color/1,colorlist/1,sorted/1],[assertions,regtypes,clpq,sr/bfall]).

Defining properties in functional notation

This next example shows the same properties as the last example but written using functional notation. The definitions are equivalent, functional syntax being just syntactic sugar.

:- module(_,[colorlist/1,sorted/1,color/1],[assertions,regtypes,fsyntax]).

% Defining some types and properties (using functional syntax)
% which can then be used in assertions. 

:- regtype color/1.
color := red | green | blue.

:- regtype colorlist/1.
colorlist := [] | [~color|~colorlist].

:- prop sorted/1.
sorted := [] | [_].
sorted([X,Y|T]) :- X .>=. Y, sorted([Y|T]).

Using the properties defined

In the following example we add some simple definitions for p/1 and q/1:

%! \begin{code}
:- module(_,[p/1,colorlist/1,sorted/1,color/1],[assertions,regtypes,fsyntax]).

% Defining some types and properties (using functional syntax)
% which are then used in two simple assertions. The system
% detects that property sorted is incompatible with the success
% type of p/1.

:- pred p(X) => sorted(X).
p(X) :- q(X).

:- pred q(X) => color(X).
q(M) :- M = red.

:- regtype color/1.
color := red | green | blue.

:- regtype colorlist/1.
colorlist := [] | [~color|~colorlist].

:- prop sorted/1.
sorted := [] | [_].
sorted([X,Y|T]) :- X >= Y, sorted([Y|T]).
%! \end{code}
%! \begin{opts}
V,output=on,filter=check_pred
%! \end{opts}

We also added a pred assertion for q/1, meaning ''in all calls q(X) that succeed, X is instantiated on success to a term of color type''. This is verified by CiaoPP.

We have also added an assertion for p/1 meaning ''in all calls p(X) that succeed, X gets instantiated to a term meeting the sorted property.''

CiaoPP detects that such assertion is false and shows the reason: the analyzer (with the eterms abstract domain eterms) infers that on success X gets bound to red, expressed as the automatically inferred regular type rt27/1, and CiaoPP finds that rt27(X) and sorted(X) are incompatible (empty intersection of the set of terms they represent):

WARNING (ctchecks_pp_messages): (lns 22-22) At literal 1 could not verify assertion:
:- check calls A>B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:>(A,B) :

[eterms] basic_props:term(A),basic_props:term(B),basic_props:term(A) 

[shfr]   native_props:mshare([[A],[A,B],[A,B,A],[A,A],[B],[B,A],[A]]) 

ERROR (ctchecks_pred_messages): (lns 3-8) False assertion:
:- check success p(X)
   => sorted(X).
because the success field is incompatible with inferred success:
[eterms] rt27(X) 
with:

:- regtype rt27/1.
rt27(red).

ERROR (auto_interface): Errors detected. Further preprocessing aborted.

Using the properties defined

In the following program:

:- module(_,[p/1,colorlist/1,sorted/1,color/1],[assertions,regtypes,fsyntax]).

% Defining some types and properties (using functional syntax)
% which are then used in two simple assertions. With default domain
% sorted/1 is not proved and will generate a run-time check and 
% optionally initiate assertion-based test generation.

:- pred p(X) => sorted(X).
p(X) :- q(X).

:- pred q(X) => list(X).
q(M) :- M = [_,_,_].

:- regtype color/1.
color := red | green | blue.

:- regtype colorlist/1.
colorlist := [] | [~color|~colorlist].

:- prop sorted/1.
sorted := [] | [_].
sorted([X,Y|T]) :- X >= Y, sorted([Y|T]).

We have changed q/1 to instantiate its argument to a list. Now CiaoPP does not flag an error, but simply warns that it cannot verify the assertion for p/1:

WARNING (ctchecks_pred_messages): (lns 3-8) Could not verify assertion:
:- check success p(X)
   => sorted(X).
because
    incompatible_type_f_fixed:sorted(X)
could not be derived from inferred success:
[eterms] rt27(X) 
with:

:- regtype rt27/1.
rt27([A,B,C]) :-
    term(A),
    term(B),
    term(C).


[shfr]   native_props:mshare([[X]]) 

WARNING (ctchecks_pp_messages): (lns 22-22) At literal 1 could not verify assertion:
:- check calls A>B
   : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
because on call arithmetic:>(A,B) :

[eterms] basic_props:term(A),basic_props:term(B),basic_props:term(A) 

[shfr]   native_props:mshare([[A],[A,B],[A,B,A],[A,A],[B],[B,A],[A]])

Indeed, the success type rt27(X) inferred for p/1 (lists of three arbitrary terms) and sorted(X) are now compatible, and thus no error is flagged. However, rt27(X) does not imply sorted(X) for all X's, and thus sorted(X) is not verified (with the default set of abstract domains).

In this case, the system will (optionally) introduce a run-time check so that sorted(X) is tested when p/1 is called. Furthermore, the system can run unit tests or generate test cases (in this case arbitrary terms) automatically to exercise such run-time tests.

An example with more complex properties

To follow this part of the tutorial we recommend to have installed CiaoPP as many of the advanced features are not yet included in the playground. An example with more complex properties (also using the functional syntax package) is shown here:

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

% Naive reverse with some complex assertions.
% The system flags a (cost) error reminding us that 
% nrev/2 is quadratic, not linear. 
% (Requires cost-related domains.)

:- pred nrev(A,B) : (list(num,A), var(B)) => list(B) 
   + ( det, terminates, steps_o( length(A) ) ).

nrev( [] )    := [].
nrev( [H|L] ) := ~conc( ~nrev(L),[H] ). 


:- pred conc(A,B,C) + ( det, terminates, steps_o(length(A))).

conc( [],    L ) := L. 
conc( [H|L], K ) := [ H | ~conc(L,K) ].

It includes a user-provided assertion stating (among other properties) that the cost of nrev/2 in resolution steps, for calls to nrev(A, B) with A a ground list and B a free variable, should be linear in the length of the (input) argument A (O(length(A)), property steps_o(length(A)) in the + field. CiaoPP can infer that this is false:

:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- false comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_o(length(A)) ).

:- checked calls conc(A,B,C).

:- checked comp conc(A,B,C)
   + ( det, terminates, steps_o(length(A)) ).

If we continue to examine the output of CiaoPP we can see this other assertion:

:- true pred nrev(A,B)
   : ( list(num,A), var(B) )
   => ( list(num,A), list(num,B),
        size_lb(length,B,length(A)),
        size_ub(length,B,length(A)) )
   + ( steps_lb(0.5*exp(length(A),2)+1.5*length(A)+1), steps_ub(0.5*exp(length(A),2)+1.5*length(A)+1) ).

The assertion explains that the stated worst case asymptotic complexity is incompatible with the quadratic lower bound cost inferred by the analyzer (in fact: $\frac{1}{2} \ length{(A)}^2 + \frac{3}{2} \ length(A) + 1$, see the steps_lb property). If we change the assertion to specify a quadratic upper bound:

:- pred nrev(A,B) : (list(num,A), var(B)) => list(B) 
   + ( det, terminates, steps_o( exp(length(A), 2) ) ).

it is now proven:

:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- checked comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_o(exp(length(A),2)) ).

:- checked calls conc(A,B,C).

:- checked comp conc(A,B,C)
   + ( det, terminates, steps_o(length(A)) ).

Now we have changed the assertion for conc/3 from complexity order (_o) to a concrete upper bound (_ub), and the system detects the error:

:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- checked comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_o(exp(length(A),2)) ).

:- checked calls conc(A,B,C).

:- false comp conc(A,B,C)
   + ( det, terminates, steps_ub(length(A)) ).

length(A) is not a correct upper bound because, as shown in the message, it is incompatible with the lower bound length(A) + 1 inferred by the analyzer:

:- true pred conc(A,B,C)
   : ( list(num,A), rt4(B), var(C) )
   => ( list(num,A), rt4(B), list1(num,C),
        size_lb(length,C,length(B)+length(A)),
        size_ub(length,C,length(B)+length(A)) )
   + ( steps_lb(length(A)+1), steps_ub(length(A)+1) ).

If we change the upper bound to length(A) + 1, then the assertion is verified.

:- checked calls nrev(A,B)
   : ( list(num,A), var(B) ).

:- checked success nrev(A,B)
   : ( list(num,A), var(B) )
   => list(B).

:- checked comp nrev(A,B)
   : ( list(num,A), var(B) )
   + ( det, terminates, steps_ub(exp(length(A),2)) ).

:- checked calls conc(A,B,C).

:- checked comp conc(A,B,C)
   + ( det, terminates, steps_ub(length(A)+1) ).