☰

Examples of types, modes, and resources in CiaoPP

Author(s): The Ciao Development Team.

The Ciao assertions model involves the combination of a rich assertion language, allowing a very general class of (possibly undecidable) properties, and a novel methodology for dealing with such assertions. This methodology is based on making a best effort to infer and check assertions statically, using rigorous static analysis tools based on safe approximations, in particular via abstract interpretation. This implies accepting that complete verification or error detection may not always be possible and run-time checks may be needed. This approach allows dealing in a uniform way with a wide variety of properties which includes types, but also, e.g., rich modes, determinacy, non-failure, sharing/aliasing, term linearity, cost etc., while at the same time allowing assertions to be optional.

The Ciao model and language design also allows for a smooth integration with testing. Moreover, as (parts of) tests that can be verified at compile time are eliminated, some tests can be passed without ever running them. Finally, the model supports naturally assertion-based test case generation.

In the following we illustrate these aspects of the Ciao assertions model through examples run on the system. While there are several ways to use the system, the idea is to have installed Ciao on your computer, including the development environment (see Installation for more information). This includes CiaoPP. You can then access CiaoPP from the Emacs interface or the command line. The examples can be also followed by running CiaoPP directly on your browser through the Ciao playground. To this end, load the examples into the playground by pressing the ↗ button (''Load in playground''), and then CiaoPP can be run clicking the More... button and selecting Analyze and check assertions. Or, you can also interact with the code boxes (you will identify them by a question mark (?) in the right top corner), and by clicking the question mark you would be able to run CiaoPP and see fragments of the analysis output.

A first example. 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.

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.

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

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, the modes for qsort/2 in the last example are expanded by the modes package (see module declaration in the above examples) to: 

:- pred qsort(X,Y) : list(num,X) => list(num,Y) + semidet.
All the assertions in the last example 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.

In the next 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 veryfied by the sustem). 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}
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. 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 srt/fall. 
:- module(_,[color/1,colorlist/1,sorted/1],[assertions,regtypes,clpq,sr/bfall]).
The 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 functiomal 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]).
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 functiomal syntax)
% which are then used in two simple assertions. The system
% detects that property sorted is incompatible with the success
% tyoe 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}
and 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.

In the program, 

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

% Defining some types and properties (using functiomal 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 the definition of incompatibility, and now CiaoPP 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]])

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 (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: , 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) ).

Generated with LPdoc using Ciao