Checking predicate app/3

Analyzing

Let us analyze this implementation of the app/3 predicate:

%! \begin{code}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => var(C).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).  
%! \end{code}
%! \begin{opts}
A,filter=all
%! \end{opts}  

By default, CiaoPP analyzes programs with a type domain (eterms) and a sharing/freeness domain (shfr). The inferred information is expressed with (true) assertions (for a more extensive tutorial of the assertion language see section Using assertions for preprocessing programs in the CiaoPP manual). true represents abstractions of the behaviour of the program inferred by the analyzer. In this case, it was inferred:

:- true pred app(A,B,C)
   : mshare([[A],[A,B],[A,B,C],[A,C],[B],[B,C],[C]])
   => mshare([[A,B,C],[A,C],[B,C]]).

:- true pred app(A,B,C)
   : ( list(A), list(B), term(C) )
   => ( list(A), list(B), list(C) ).

The first assertion contains types information and encodes predicate app/3 is called with A and B as lists and if it succeeds, C will be a list.

The second one contains information about how variables are shared. It was inferred that when app(A,B,C) is called arguments A, B, and C may be shared and if it succeeds they also will be shared, since C is the concatenation of A and B.

Assertion Checking

In the example above, we have also added an assertion with properties that we want to prove about the execution of the program.

:- pred app(A,B,C) : (list(A), list(B)) => var(C).

ERROR (ctchecks_pred_messages): (lns 3-3) False assertion:
:- check success app(A,B,C)
   : ( list(A), list(B) )
   => var(C).
because the success field is incompatible with inferred success:
[eterms] basic_props:list(A),basic_props:list(B),basic_props:list(C) 


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

Assertion checking can also be reported within the source code, we can see that the analyzer does not verify the assertion that we had included. Run the analysis again (clicking ? button) to see the result.

%! \begin{code}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => var(C).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).  
%! \end{code}
%! \begin{opts}
solution=verify_assert
%! \end{opts}  
%! \begin{solution}
:- module(_, [app/3], [assertions]).

:- pred app(A,B,C) : (list(A), list(B)) => list(C).

app([],Y,Y). 
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).   
%! \end{solution}

Program Optimization

The following program naively implements a predicate that duplicates the first element of a list.

%! \begin{code}
:- module(_, [dup_first/2], []).

dup_first([X|Xs], Zs) :-
    app([X], [X|Xs], Zs).

app([],Y,Y).
app([X|Xs], Ys, [X|Zs]) :-
    app(Xs,Ys,Zs).
%! \end{code}
%! \begin{opts}
O,filter=all
%! \end{opts}