CiaoPP Tutorials
****************

This document/site groups a number of interactive tutorials meant to
help when starting to use 'CiaoPP'.  It is a companion to the reference
manual for 'CiaoPP', which gives a fuller description of the system.

Indexes

Introduction
************

This document groups a number of tutorials meant to help when starting
to use 'CiaoPP'.  It is a companion to the reference manual for
'CiaoPP', which gives a fuller description of the system.  Some of these
tutorials are interactive, using the Active Logic Documents facility of
'LPdoc'.

The following tutorials are available:

   * CiaoPP at a glance.  This brief tutorial provides a quick
     overview suitable for understanding the some basics about how
     'CiaoPP' works.  It is however is not intended to be a tutorial on
     how to use 'CiaoPP'.  The following tutorial is recommended for
     this.

   * A Gentle Introduction to Static Verification and Bug Finding with CiaoPP.
     This tutorial illustrates step-by-step the
     development of a concrete program starting from a given problem
     statement and a specification, expressed using the 'Ciao' assertion
     language, to describe predicates and their properties.  Our aim is
     to show how to use 'CiaoPP' to prove statically whether these
     assertions hold and/or detect bugs, while stepwise developing the
     program.  The tutorial also provides an introduction to the dynamic
     checking aspects of 'CiaoPP'.  In particular, the document includes
     the following topics:

        * Defining modules and exports
        * Type and Mode Analysis
        * Assertions and properties
        * Non-failure and Determinacy Analysis
        * Dynamic Bug Finding with 'CiaoPP''s Testing Facilities

   * Program Development using the CiaoPP Program Processor is a
     more advanced tutorial.  The tutorial includes these sections:

        * Static Analysis and Program Assertions
             * Static Analysis Basics
             * Type Analysis
             * Non-failure and Determinacy Analysis
             * Size, Resources, and Termination Analysis
             * Decidability, Approximations, and Safety

        * Program Debugging and Assertion Checking
             * Assertions and Properties
             * Using analysis information for debugging
             * Static Checking of Assertions in System Libraries
             * Static Checking of User Assertions and Program Validation
             * Performance Debugging and Validation

About CiaoPP
============

CiaoPP is the abstract interpretation-based preprocessor of the Ciao
multi-paradigm program development environment.  CiaoPP can perform a
number of program debugging, analysis, and source-to-source
transformation tasks on (Ciao) Prolog programs.  These tasks include:

   * Inference of properties of the predicates and literals of the
     program, including types, modes and other variable instantiation
     properties, non-failure, determinacy, bounds on computational cost,
     bounds on sizes of terms in the program, etc.

   * Certain kinds of static debugging and verification, finding errors
     before running the program.  This includes checking how programs
     call system library predicates and also checking the assertions
     present in the program or in other modules used by the program.
     Such assertions represent essentially partial specifications of the
     program.

   * Several kinds of source to source program transformations such as
     program specialization, slicing, partial evaluation of a program,
     program parallelization (taking granularity control into account),
     inclusion of run-time tests for assertions which cannot be checked
     completely at compile-time, etc.

   * The abstract model of the program inferred by the analyzers can be
     used to certify that untrusted mobile code is safe w.r.t.  a given
     policy (this implements the abstraction-carrying code approach to
     mobile code safety).

The information generated by analysis, program properties to be
verified, descriptions of the system libraries, directives provided to
guide analysis, etc.  are all written in the same assertion language,
which is in turn also processed by the Ciao system documentation
generator, 'lpdoc'.

CiaoPP is distributed under the GNU general public license.

CiaoPP at a glance
******************

Author(s): Isabel Garcia-Contreras, Daniela Ferreiro.

The purpose of this document is to quickly illustrate some of the kinds
of static processing that 'CiaoPP' can perform.  Note that this is not
intended to be a tutorial, for that please follow A Gentle Introduction to Static Verification and Bug Finding with CiaoPP
or
Program Development using the CiaoPP Program Processor.

Setup
=====

In order to follow these examples you need to either:

   * Install 'Ciao' on your computer, including the development
     environment (see Installation for more information).  This
     includes 'CiaoPP' (and 'LPdoc').  You can then access 'CiaoPP' from
     the Emacs interface or the command line.

   * Run '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>.

The instructions below use the Emacs interface but the steps can also be
performed in the playground version.

Analyzing
=========

Let us analyze this implementation of the append predicate:

     :- 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).
Automatic analysis can be performed by using the direct access button in
the Emacs interface [ciaopp_tutorials.cachedoc/texinfo/quick-ciaoanalysis_autofig].

By default, 'CiaoPP' analyzes programs with a type domain ('eterms') and
a sharing/freeness (modes) domain ('shfr').  We can open the file with
the inferred information by typing 'C-c C-v'.

The inferred information is expressed with ('true') assertions (for a
more extensive tutorial of the assertion language see Using assertions for preprocessing programs).
Assertion marked as 'true'
contain safe approximations (safe abstractions) of the behavior of the
program that were inferred by the analyzer.  In this case 'CiaoPP'
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 type information and expresses the fact
that predicate 'app/3' is called (':' field) with 'A' and 'B' bound to
'lists' and, if it succeeds ('=>' field), then 'C' will be a 'list'.

The second assertion 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,
sice '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).
This assertion is stating that if predicate 'append/3' is called with
'A' and 'B' bound to 'list's, then, if the call succeeds, 'C' will be a
free variable.  This is not true in general of course.  We can check
this assertion by clicking the [ciaopp_tutorials.cachedoc/texinfo/quick-ciaoasr_autofig] icon in the Emacs interface and we
obtain:

     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.

Since this assertion does not hold we get a message saying so.

Assertion checking can also be reported within the source code.  If we
open the output file the 'CiaoPP' produces ('C-c C-v'), we see that the
analyzer proves the assertion that we had included false:

     :- checked calls app(A,B,C)
        : ( list(A), list(B) ).

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

So we correct it with:

     :- pred app(A,B,C) : (list(A), list(B)) => list(C).
and run the analysis again.  In this case we get no error messages and,
as before, results can also be reported in the source file:

     :- checked calls app(A,B,C)
        : ( list(A), list(B) ).

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

Program Optimization
====================

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

     :- 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).
'CiaoPP' can automatically optimize sources by using the [ciaopp_tutorials.cachedoc/texinfo/quick-ciaopt_autofig] button:

     :- module(_1,[dup_first/2],[assertions]).

     dup_first([A|B],[A,A|B]).

Advanced Preprocessing
======================

'CiaoPP' has several parameters for each of the main actions.  For more
information, see the Program Development using the CiaoPP Program Processor.

A Gentle Introduction to Static Verification and Bug Finding with CiaoPP
************************************************************************

Author(s): Daniela Ferreiro, Jose F. Morales (minor).

This is a tutorial to illustrate step-by-step the development of a
program for a given specification, using the 'Ciao' language of
assertions, which allows the user to describe predicates and properties.
Our aim is to show how to use 'CiaoPP' to prove statically whether these
assertions hold and/or detect bugs.  The tutorial also provides an
introduction to the dynamic checking aspects of 'CiaoPP'.  Although the
solution of the different exercises is provided in this tutorial, try to
think first about the answer on your own, and experiment!

Consider the following specification (taken from the Prolog programming
contest at ICLP'95, Portland, USA):

Specification.  Write a predicate 'powers/3', which is called with a
list of non-negative numbers as first argument, a non-negative number
'N' as second argument, and a free third argument.  Such a call must
succeed exactly once and unify the third argument with the list that
contains the smallest 'N' integers (in ascending order) that are a
non-negative power of one of the elements of the first argument.

In the next section we will show a complete fully working Initial implementation.
If you wish, you can skip directly to this solution
and run some queries before start specifying properties Using assertions.

How to use this 'interactive' document:
   * Some code boxes needs your interaction.  You will identify them by
     a question mark (?)  in the right top corner.
   * Your goal is turn all question marks boxes into green checked marks
     (✔):
        * Boxes with a thinking face (🤔) are exercises that you must
          complete in order to progress.  Once an exercise is completed,
          press the question mark.
        * Boxes without the thinking face just needs pressing the
          question mark.  They are editable so that you can play with
          them.
        * Code errors or failed exercises turn into red erroneous mark
          (✘).  You can try again.
        * When available, pressing the northeast pointing arrow (↗) will
          load the code in a separate playground window.
   * Additionally, boxes with right-pointing triangles (▶) allow
     interacting with the code loaded so far (as queries).  In order to
     use them, make sure previous code boxes are checked.

Defining modules and exports
============================

We will start with the module declaration:
     :- module(powers,[powers/3],[assertions])
This module declaration states that the name of the module is 'powers',
that it exports a predicate 'powers/3', and that it uses the
'assertions' package.  Note that the module 'powers' will define other
predicates, such as 'remove_power/3' (the program can be found below).
These other predicates are internal to the module, i.e., they cannot be
seen or used in other modules.  One of the reasons why we export only
the predicate 'powers/3' is that during the analysis of this program,
'CiaoPP' can assume that external calls are only to this predicate.
This fact will allow 'CiaoPP' to produce more accurate information about
the program since analysis then does not have to consider all the
possible ways other predicates inside the module may be called, and only
those that can actually occur in the module.

Writing powers/3
================

Once we have defined the module we start writing the predicate
'powers/3'.  We can sketch the main idea of our approach with a
motivating example.  Consider the following query:

     ?- powers([2,3,5],7,Powers).
We start by constructing the list of pairs [(2,2),(3,3),(5,5)], which is
sorted and which has no two pairs with the same first component.  The
implementation of this predicate can be as follows:

     :- module(_, _, [assertions]).
     %! \begin{focus}
     create_pairs([],[]).
     create_pairs([X|R],[(X,X)|S]) :- create_pairs(R,S).
     %! \end{focus}
In each pair '(P,F)', 'P' is the smallest power of 'F' that is not in
the solution list yet.  So, the first component of the first element of
the pair-list is the next element in the output we are constructing.  We
remove this pair, compute the next power of 'F' (i.e., 'P'*'F') and
insert the pair '(P*F,F)' into the pair-list, respecting the invariants.
We start by writing 'remove_power/3', which takes a number as first
argument, and a list of pairs as second argument, and returns as its
third argument another pair-list consisting of the second argument minus
the pair '(P,F)' with 'P' the first argument.

     :- module(_, _, [assertions]).
     %! \begin{focus}
     remove_power(_,[],[]).
     remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
         Power =\= Power1, !.
     remove_power(Power,[_|RestPFsIn],PFsOut) :-
         remove_power(Power,RestPFsIn,PFsOut).
     %! \end{focus}
We also define 'sorted_insert/3':

     :- module(_, _, [assertions]).
     %! \begin{focus}
     sorted_insert([], X, [X]).
     sorted_insert([(X1,F1)|L1], (X,F), [(X,F), (X1,F1)|L1]) :- X =< X1, !.
     sorted_insert([P|L1], X, [P|L]) :- sorted_insert(L1, X, L).
     %! \end{focus}
This predicate compares the value of the item to be inserted (the second
argument) with the head of the list.  If it is less than this value,
then the new pair must be inserted just before this head, otherwise the
pair is inserted into the new tail.

Initial implementation
----------------------

Using the information we have seen so far we would have the following
implementation (there is a brief explanation of each predicate):

     :- module(_,[powers/3],[assertions]).

     %! \begin{focus}
     % powers(X,N,P): P is the sorted list that contains the smallest N integers
     % that are a non-negative power of one of the elements of the list X.

     powers([],_,[]).
     powers(Factors,N,Powers) :-
         quicksort(Factors, SFactors),
         create_pairs(SFactors,Pairs),
         first_powers(N,Pairs,Powers).

     % quicksort(Xs,Ys): Performs a quicksort of a list Xs and returns the result
     % in Ys.

     quicksort(Xs,Ys) :- qsort(Xs,Ys,[]).

     qsort([],DL,DL).

     qsort([X|Xs],Head,Tail) :-
         partition(Xs,X,L,R),
         qsort(L,Head,[X|QR]),
         qsort(R,QR,Tail).

     partition([],_,[],[]).
     partition([X|Xs],Pv,[X|L],R) :- X =< Pv, !, partition(Xs,Pv,L,R).
     partition([X|Xs],Pv,L,[X|R]) :- X > Pv, partition(Xs,Pv,L,R).

     % create_pairs(F,P): F is a list and P is sorted list of pairs. Each
     % element of P has the form (X,X), where X is a element of F.

     create_pairs([],[]).
     create_pairs([X|R],[(X,X)|S]) :- create_pairs(R,S).

     % first_powers(N,L,R): R is a sorted list with N non-negative numbers.

     first_powers(N,[(Power,Factor)|PFs],[Power|Powers]) :-
         N > 0, !,
         N1 is N-1,
         remove_power(Power,PFs,PFs1),
         Power1 is Power*Factor,
         sorted_insert(PFs1,(Power1,Factor),PFs2),
         first_powers(N1,PFs2,Powers).
     first_powers(0,_,[]).

     % remove_powers(P,L,R): R is the sorted list of pairs obtained by removing
     % from the list L.

     remove_power(_,[],[]).
     remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
         Power =\= Power1, !.
     remove_power(Power,[_|RestPFsIn],PFsOut) :-
         remove_power(Power,RestPFsIn,PFsOut).

     % sorted_insert(L,P,R): R is the sorted list of pairs obtained by adding
     % to the list L the pair P.

     sorted_insert([], X, [X]).
     sorted_insert([(X1,F1)|L1], (X,F), [(X,F), (X1,F1)|L1]) :- X =< X1, !.
     sorted_insert([P|L1], X, [P|L]) :- sorted_insert(L1, X, L).
     %! \end{focus}
Below are some examples queries to the 'powers/3' predicate (make sure
that the code box above is marked with a green check mark):

     ?- powers([3,5,4],17,Powers).
     ?- powers([2,9999999,9999998],20,Powers).
     ?- powers([2,4],6,Powers).
Exercise 1 (Understanding the predicate).  What is the answer of this
query?
     ?- powers([4,2],6,Powers).
Hint: Remember that Powers contains the smallest N integers (in
ascending order)

Analysis of our the initial implementation
------------------------------------------

Let us analyze this implementation of the 'powers/3' predicate.  The
'Ciao' system includes a large number of domains that can be used in
this program and has strategies for selecting between them.  But, by
default, 'CiaoPP' analyzes programs with a types domain (the regular
types domain 'eterms') and a modes domain (the sharing/freeness domain
'shfr').  We will be working mainly with these two.  The following are
the results (it is not necessary to look too carefully at these results
yet):

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

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

     [shfr]   native_props:mshare([[B],[B,A],[B,A,B],[B,B],[A],[A],[A,B],[B],[C]]),term_typing:var(A),term_typing:var(C)

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

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

     [shfr]   native_props:mshare([[B],[B,A],[B,A,B],[B,B],[A],[A],[A,B],[B],[C]]),term_typing:var(A),term_typing:var(C)

     WARNING (ctchecks_pp_messages): (lns 27-39) 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),rt188(B)
     with:

     :- regtype rt188/1.
     rt188(0).

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

     WARNING (ctchecks_pp_messages): (lns 27-39) At literal 4 could not verify assertion:
     :- check calls A is B
        : ( ( var(A), nonvar(B), var(A), arithexpression(B) ); ( var(A), nonvar(B), var(A), intexpression(B) ); ( nonvar(A), nonvar(B), num(A), arithexpression(B) ); ( nonvar(A), nonvar(B), int(A), intexpression(B) ) ).
     because on call arithmetic:is(A,B) :

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

     :- regtype rt201/1.
     rt201(A*B) :-
         term(A),
         term(B).

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

     WARNING (ctchecks_pp_messages): (lns 47-48) 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),rt112(A),basic_props:term(B),basic_props:term(B)

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

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

     [eterms] rt112(A),basic_props:term(B),basic_props:term(B),basic_props:num(A),arithmetic:arithexpression(C)

     [shfr]   native_props:mshare([[A],[A,B],[A,B,B],[A,B],[B],[B,B],[B]]),term_typing:ground([A,C])

These warnings are stating that there are a number of assertions that
cannot be shown to hold.  In particular, the analysis is saying that it
is not possible to ensure that the calls that the program makes to
predicates such as '>=/2', '</2', '>/2', 'is/2', and '=</2' respect the
corresponding preconditions or calling modes, which generally require
the arguments to be bound to arithmetic expressions when called.  The
interesting thing to note here is that we did not have to include any
assertions in our code.  The warning messages stem from the assertions
(specifications) that provide the pre-conditions and post-conditions for
such library predicates in the 'Ciao' system libraries.  Thus, a first
observation is that it is possible to identify potential bugs even
without actually adding assertions to programs.  However, in general, if
the program is incorrect, the more assertions are present in the
program, the more likely errors will be detected automatically.  Thus,
we may choose to dedicate more time to writing assertions for those
parts of the program that seem to be possibly buggy or whose correctness
is important.

In particular, in view of the warnings above, it seems useful to be able
to ensure that all these library predicates will always be called
properly within our module and thus be more confident about our program.
We can work towards this objective by providing some information
regarding how the exported predicate, 'powers/3', will be called from
outside the module.

Using assertions
================

For example, from the problem specification we know that the second
argument should always be a number.  In order to be able to state such
properties of predicates we will have to use the assertion language, in
particular (as we have just seen), 'pred' assertions which are used to
describe a particular predicate.  Such assertions use the following
syntax:

     :- pred Pred [:Precond] [=> Postcond] [+ CompProp] .
Such an assertion indicates that in any call to 'Pred', if 'Precond'
holds in the calling state and the computation of the call succeeds,
then 'Postcond' also holds in the success state.  As we will see later,
'Precond' and 'Postcond' are conjunctions of state properties.
'CompProp' refers to a sequence of states and we refer to the properties
that appear there as properties of the computation.  Examples are
determinacy, non-failure, or cost.

So, we can start by adding the following 'pred' assertion to state that
when 'powers/3' is called the second argument is bound to a number,
using the built-in property 'num/1':

     :- pred powers(A,B,C) : num(B).
We then proceed to run 'CiaoPP' again:

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

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

     [shfr]   native_props:mshare([[B],[B,A],[B,A,B],[B,B],[A],[A],[A,B],[B],[C]]),term_typing:var(A),term_typing:var(C)

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

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

     [shfr]   native_props:mshare([[B],[B,A],[B,A,B],[B,B],[A],[A],[A,B],[B],[C]]),term_typing:var(A),term_typing:var(C)

     WARNING (ctchecks_pp_messages): (lns 28-35) At literal 4 could not verify assertion:
     :- check calls A is B
        : ( ( var(A), nonvar(B), var(A), arithexpression(B) ); ( var(A), nonvar(B), var(A), intexpression(B) ); ( nonvar(A), nonvar(B), num(A), arithexpression(B) ); ( nonvar(A), nonvar(B), int(A), intexpression(B) ) ).
     because on call arithmetic:is(A,B) :

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

     :- regtype rt201/1.
     rt201(A*B) :-
         term(A),
         term(B).

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

     WARNING (ctchecks_pp_messages): (lns 39-40) 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),rt112(A),basic_props:term(B),basic_props:term(B)

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

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

     [eterms] rt112(A),basic_props:term(B),basic_props:term(B),basic_props:num(A),arithmetic:arithexpression(C)

     [shfr]   native_props:mshare([[A],[A,B],[A,B,B],[A,B],[B],[B,B],[B]]),term_typing:ground([A,C])

As we can see, 'CiaoPP' continues producing some warning messages but
they are now fewer.

Regular types and other properties
==================================

We have seen before how certain types can be used as properties to
describe predicates.  In 'CiaoPP' we can define new regular types using
'regtype' declarations.  In general, properties (such as these types)
are normal predicates, but which meet certain conditions (e.g.,
termination) and are marked as such via 'prop/1' or 'regtype/1'
declarations).  Other properties like 'num/1', 'var/1', or 'not_fails'
are builtins, defined in libraries.  See Declaring regular types
in the 'CiaoPP' manual for more details on (regular) types, as well as
other details about properties in 'Ciao').  For example, our
specification states that the first argument is a list of numbers.  This
property is available in the 'Ciao' libraries, however, we choose to
declare it ourselves.  So we represent the set of "lists of numbers" by
the regular type 'list_num', defined as follows:

     :- regtype list_num(X) # "@var{X} is a list of numbers." .
     list_num([]).
     list_num([X|T]) :-
           num(X), list_num(T).

The problem specification also tells us that the first argument is a
list of numbers and that 'powers/3' returns another number list of
numbers (for now, we will not put other restrictions such as being a
list of non-negative numbers).  I.e., combining with the previous
information, we need to ensure that for any call to predicate 'powers/3'
with the first argument bound to a list of numbers, the second argument
bound to a number, and the third one unbound, if the call succeeds, then
the third argument will also be bound to a list of numbers.

Exercise 2 (Solved).  What assertion would we need to add?
     %! \begin{code}
     :- pred powers(A,B,C) : (?, ?, ?) => (?) .
     %! \end{code}
     %! \begin{opts}
     solution=equal
     %! \end{opts}
     %! \begin{solution}
     :- pred powers(A,B,C) : (list_num(A), num(B), var(C)) => (list_num(C)).
     %! \end{solution}

If we now take a look into the file generated by 'CiaoPP' we will find
that there are no warnings, i.e., 'CiaoPP' can now prove that all calls
to library predicates are correct and will not raise any errors at run
time (we will return to this topic later).  Furthermore, we will find in
the output the following assertion:

     %% %% :- check pred powers(A,B,C)
     %% %%    : ( list_num(A), num(B), var(C) )
     %% %%    => list_num(C).

     :- checked calls powers(A,B,C)
        : ( list_num(A), num(B), var(C) ).

     :- checked success powers(A,B,C)
        : ( list_num(A), num(B), var(C) )
        => list_num(C).

This means that the assertion that we have included has been marked as
checked, i.e., it has been validated, proving that indeed the third
argument of 'powers/3' will be bound to a list on success.

If we take a look again into the file generated by 'CiaoPP' we will find
these assertions:

     :- true pred remove_power(_1,_A,PFsOut)
        : ( num(_1), list(^(('basic_props:num','basic_props:num')),_A), term(PFsOut) )
        => ( num(_1), list(^(('basic_props:num','basic_props:num')),_A), list(^(('basic_props:num','basic_props:num')),PFsOut) ).

     :- true pred remove_power(_1,_A,PFsOut)
        : ( mshare([[PFsOut]]),
            var(PFsOut), ground([_1,_A]) )
        => ground([_1,_A,PFsOut]).

The sharing and freeness analysis abstract domain computes freeness,
independence, and grounding dependencies between program variables.  The
second assertion expresses that the third argument is a free variable
while the first and second arguments are input values (i.e., ground on
call) when 'remove_power/3' is called (:).  Upon success, all three
arguments will get instantiated.  On the other hand, the first assertion
expresses that, if 'remove_power(N, A, B)' is called with a number 'N',
a pair-list of numbers in 'A' and any term in 'B', then 'B' will on exit
be a pair-list of numbers.  Therefore, we need a regular type
'list_pair' which defines a list of pairs '(X,Y)'.  If we continue to
examine the output of 'CiaoPP' we can see this other assertion:

     :- true pred sorted_insert(_A,X,_B)
        : ( list(^(('basic_props:num','basic_props:num')),_A), rt96(X), term(_B) )
        => ( list(^(('basic_props:num','basic_props:num')),_A), rt96(X), list1(^((num,num)),_B) ).

     :- regtype rt51/1.

     rt51([]).
     rt51([A|B]) :-
         num(A),
         term(B).

     :- regtype rt96/1.

     rt96((A,B)) :-
         num(A),
         num(B).

Where we find new types, inferred by 'CiaoPP'.  The analyzer thus tells
us about types that represent the data that the program builds, and we
can use these definitions back in the source file to enhance the
specification.  In our case, the second regular type is defining the
pairs, so we can copy it into the source file, giving it a meaningful
name for clarity, as follows:

     :- regtype num_pair(P) .
     num_pair((X, Y)):-
         num(X),
         num(Y).

     :- regtype list_pair(L) .
     list_pair([]).
     list_pair([X|Xs]):-
         num_pair(X),
         list_pair(Xs).

     :- regtype list_pair1(L) .
     list_pair1([X|Xs]):-
        num_pair(X),
        list_pair(Xs).

(Note that we can also use parametric types here, but we use a simple
type for simplicity.)  Once we have defined these regular types, we can
write more precise assertions:

Exercise 3.  What assertion would we need to add?
     %! \begin{code}
     :- pred remove_power(A,B,C) : (?, ?, ?) => (?) .
     %! \end{code}
     %! \begin{opts}
     solution=equal
     %! \end{opts}
     %! \begin{solution}
     :- pred remove_power(A,B,C) : (num(A), list_pair(B), var(C)) => list_pair(C).
     %! \end{solution}
Hint: 'remove_power/3' is called in this program with the first
parameter being a number, the second argument being of type 'list_pair'
(i.e., bound to a list of pairs) and one variable.  And on success the
third argument is bound to a 'list-pair'.

Exercise 4.  What assertion would we need to add?
     %! \begin{code}
     :- pred sorted_insert(A,B,C) : (?, ?, ?) => (?) .
     %! \end{code}
     %! \begin{opts}
     solution=equal
     %! \end{opts}
     %! \begin{solution}
     :- pred sorted_insert(A,B,C) : (list_pair(A), num_pair(B), var(C)) => list_pair1(C).
     %! \end{solution}
Hint: 'sorted_insert/3' is called in this program with the first
parameter being of type 'list_pair' (i.e., bound to a pair-list), the
second argument being of type 'num_pair' ( i.e., bound to a pair of
numbers) and one variable.  And on success the third argument is bound
to a non-empty list-pair.

Using the information we have seen so far we would have the following
implementation:

     :- module(_,[powers/3],[assertions, regtypes, nativeprops]).

     %! \begin{focus}
     :- regtype list_num(X) .
     list_num([]).
     list_num([X|T]) :-
         num(X),
         list_num(T).

     % powers(X,N,P): P is the sorted list that contains the smallest N integers
     % that are a non-negative power of one of the elements of the list X.
     :- pred powers(A,B,C) : (list_num(A), num(B), var(C)) => (list_num(C)).

     powers([],_,[]).
     powers(Factors,N,Powers) :-
         quicksort(Factors, SFactors),
         create_pairs(SFactors,Pairs),
         first_powers(N,Pairs,Powers).

     %! quicksort(Xs,Ys): Performs a quicksort of a list `Xs` and returns the
     % result in Ys`.

     quicksort(Xs,Ys) :- qsort(Xs,Ys,[]).

     qsort([],DL,DL).

     qsort([X|Xs],Head,Tail) :-
         partition(Xs,X,L,R),
         qsort(L,Head,[X|QR]),
         qsort(R,QR,Tail).

     partition([],_,[],[]).
     partition([X|Xs],Pv,[X|L],R) :- X =< Pv, !, partition(Xs,Pv,L,R).
     partition([X|Xs],Pv,L,[X|R]) :- X > Pv, partition(Xs,Pv,L,R).

     %! create_pairs(F,P): `F` is a list and `P` is sorted list of pairs.
     %  Each element of `P` has the form `(X,X)`, where `X` is a element of `F`.

     create_pairs([],[]).
     create_pairs([X|R],[(X,X)|S]) :- create_pairs(R,S).

     :- regtype num_pair(P) .
     num_pair((X, Y)):- num(X), num(Y).

     :- regtype list_pair(L).
     list_pair([]).
     list_pair([X|Xs]):-
         num_pair(X),
         list_pair(Xs).

     :- regtype list_pair1(L).
     list_pair1([X|Xs]):-
        num_pair(X),
        list_pair(Xs).

     %! first_powers(N,L,R): `R` is a sorted list with `N` non-negative numbers.
     %  includedef{first_powers/3}

     :- pred first_powers(A,B,C) : (num(A), list_pair(B),var(C)) => (list_num(C)) .

     first_powers(N,[(Power,Factor)|PFs],[Power|Powers]) :-
         N > 0, !,
         N1 is N-1,
         remove_power(Power,PFs,PFs1),
         Power1 is Power*Factor,
         sorted_insert(PFs1,(Power1,Factor),PFs2),
         first_powers(N1,PFs2,Powers).
     first_powers(0,_,[]).

     %! remove_powers(P,L,R): `R` is the sorted list of pairs obtained by removing from the list `L`
     %  the pair (`P`,_).

     :- pred remove_power(A,B,C) : (num(A), list_pair(B), var(C)) => list_pair(C) .

     remove_power(_, [], []).
     remove_power(Power, [(Power1, Factor)|RestOut], [(Power1, Factor)|RestOut]) :-
         Power == Power1, !.
     remove_power(Power, [_|RestPFsIn], PFsOut) :-
         remove_power(Power, RestPFsIn, PFsOut).

     %! sorted_insert(L,P,R): `R` is the sorted list of pairs obtained by adding to the list `L`
     %  the pair `P`.

     :- pred sorted_insert(A,B,C) : (list_pair(A), num_pair(B), var(C)) => list_pair1(C) .

     sorted_insert([], X, [X]).
     sorted_insert([(X1,F1)|L1], (X,F), [(X,F), (X1,F1)|L1]):- X =< X1, !.
     sorted_insert([X1|L1], X, [X1|L]):- sorted_insert(L1, X, L).
     %! \end{focus}

Bugs detected by CiaoPP
=======================

In the sections above we have included assertions to describe some
properties that we require to hold of our program.  But we also
mentioned that 'CiaoPP' can identify errors without these assertions.
So imagine we make some modifications to the predicate 'remove_power/3'
defined above:

     :- module(_,[remove_power/3],[assertions]).

     remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
         Power =\= power1, !.
     remove_power(Power,[_|RestPFsIn],PFsOut) :-
         remove_power(Power,RestPFsIn,PFsOut1).

If we now run 'CiaoPP' it produces the following output:

     WARNING: (lns 5-6) [PFsOut,PFsOut1] - singleton variables in remove_power/3

     WARNING (preproc_errors): (lns 2-4) goal arithmetic:=\=(Power,power1) at literal 1 does not succeed!

     WARNING (preproc_errors): (lns 5-6) goal remove_power_bug1:remove_power(Power,RestPFsIn,PFsOut1) at literal 1 does not succeed!

     ERROR (ctchecks_pp_messages): (lns 2-4) At literal 1 false assertion:
     :- check calls A=\=B
        : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
     because on call arithmetic:=\=(A,B) :

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

     :- regtype rt2/1.
     rt2(power1).

As we can see, different messages appear.  In this section, we will
explain one by one what each of these messages indicates, and how we can
handle them:

   * Singleton variable: The first message is a warning message which
     indicates that there are singleton variables.  We know that the
     singleton variables are those which appear only one time in a
     clause.  As mistyping a variable is a common mistake, for this
     reason, 'CiaoPP' outputs a warning message indicating if a variable
     is used only once (such warnings would also be emitted by the
     compiler).

     Exercise 5 (Detecting Bugs).  What variable do you need to change?
     (Only change the incorrect variable.)
          :- module(_,[remove_power/3],[assertions]).
          %! \begin{code}
          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut1).
          %! \end{code}
          %! \begin{opts}
          solution=errors,message=singleton
          %! \end{opts}
          %! \begin{solution}
          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut).

          % In our case, we type PFsOut1 instead of PFsOut.
          %! \end{solution}

   * No base case: The fact that a predicate always fails is not
     sufficient to conclude that there is a bug in the program.
     However, in most cases this is actually a bug, as is the case in
     this program.  Predicate 'remove_power/3' is called recursively but
     has no base case, this means it will either loop or fail.  So, we
     add the following base case and fix the error:

          :- module(_,[remove_power/3],[assertions]).

          remove_power([],[]).
          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut).

     We now obtain the following messages:

          WARNING: (lns 4-5) predicate remove_power/3 is already defined with arity 2

          WARNING (preproc_errors): (lns 4-5) goal arithmetic:=\=(Power,power1) at literal 1 does not succeed!

          WARNING (preproc_errors): (lns 6-7) goal remove_power_bug3:remove_power(Power,RestPFsIn,PFsOut) at literal 1 does not succeed!

          ERROR (ctchecks_pp_messages): (lns 4-5) At literal 1 false assertion:
          :- check calls A=\=B
             : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
          because on call arithmetic:=\=(A,B) :

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

          :- regtype rt2/1.
          rt2(power1).

   * Arity: We have forgotten a parameter in the base case of the
     recursive predicate 'remove_power/3'.  Then, 'CiaoPP' detects that
     two predicates: 'remove_power/2' and 'remove_power/3' are defined,
     so it is possible that we have forgotten or added an argument in
     one of them (these warnings are also detected by the compiler and
     can also be turned off when using multi-arity predicates).

     Exercise 6 (Detecting Bugs).  What is the correct base case?
          %! \begin{code}
          :- module(_,[remove_power/3],[assertions]).

          remove_power([],[]).
          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut).
          %! \end{code}
          %! \begin{opts}
          solution=errors,message=arity
          %! \end{opts}
          %! \begin{solution}
          :- module(_,[remove_power/3],[assertions]).

          remove_power(_,[],[]).
          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut).
          %! \end{solution}

     We run again 'CiaoPP':
          ERROR (ctchecks_pp_messages): (lns 4-5) At literal 1 false assertion:
          :- check calls A=\=B
             : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
          because on call arithmetic:=\=(A,B) :

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

          :- regtype rt9/1.
          rt9(power1).

   * Static Checking of Assertions in System Libraries: As mentioned
     before, 'CiaoPP' can find incompatibilities between the ways in
     which library predicates are called.  In our example '=\=/2' is a
     library predicate so suppose that incidentally a bug was introduced
     in the second clause of 'remove_power/3', and instead of writing
     'Power1' we write 'power1' (It is a bug since variables always
     begin with a capital letter).  'CiaoPP' tells us that the
     'arithmetic' library in 'Ciao' contains an assertion of the form:
          :- check calls A=\=B : ( nonvar(A), nonvar(B), arithexpression(A), arithexpression(B) ).
     which requires the second argument of '=\=/2' to be an arithmetic
     expression (which is a regular type also defined in the arithmetic
     library) that contains no variables.  Moreover, the 'eterms'
     analysis indicates us that in our program 'A' is any term and 'B'
     is an auxiliary regular type which was created by 'CiaoPP' to
     represent the term 'power1'.

     Exercise 7 (Detecting Bugs).  Although we have seen the predicate
     without bugs, try to write it again without any error.
          :- module(_,[remove_power/3],[assertions, regtypes, nativeprops]).

          :- regtype list_num(X).
          list_num([]).
          list_num([X|T]) :-
                num(X), list_num(T).

          :- regtype list_num1(X).
          list_num1([X|T]) :-
              num(X),
              list_num(T).

          :- regtype num_pair(P).
          num_pair((X, Y)) :- num(X), num(Y).

          :- regtype list_pair(L).
          list_pair([]).
          list_pair([X|Xs]) :-
              num_pair(X),
              list_pair(Xs).

          :- regtype list_pair1(L).
          list_pair1([X|Xs]) :-
             num_pair(X),
             list_pair(Xs).
          %! \begin{code}
          :- pred remove_power(A,B,C) : (num(A), list_pair(B), var(C)) => list_pair(C).

          remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
              Power =\= power1, !.
          remove_power(Power,[_|RestPFsIn],PFsOut) :-
              remove_power(Power,RestPFsIn,PFsOut1).
          %! \end{code}
          %! \begin{opts}
          solution=errors
          %! \end{opts}
          %! \begin{solution}
          :- pred remove_power(A,B,C) : (num(A), list_pair(B), var(C)) => list_pair(C).

          remove_power(_, [], []).
          remove_power(Power, [(Power1, Factor)|RestOut], [(Power1, Factor)|RestOut]) :-
              Power =\= Power1, !.
          remove_power(Power, [_|RestPFsIn], PFsOut) :-
              remove_power(Power, RestPFsIn, PFsOut).
          %! \end{solution}

Nonfailure+Determinism Domain
=============================

So far we have only worked with the two most used abstract domains:
'shfr' and 'eterms'.  However, 'CiaoPP' has a wide variety of abstract
domains to perform analysis with.  In this section, we will analyze the
example with 'nfdet' analysis.  The 'nfdet' combined domain carries
nonfailure ('nf') and determinism ('det') information, i.e., the
analysis will be able to detect procedures that can be guaranteed not to
fail (produce at least one solution) and to detect predicates which are
deterministic (produce at most one solution).

Categories
----------

The following lattice diagram summarizes several determinacy and
nonfailure properties inferred by the 'nf' and 'det' domains:

               nondet [0,inf]
               /        \
              /          \
          semidet [0,1]  multi [1,inf]
             /       \     /
            /         \   /
         fails [0,0]   det [1,1]
                 \      /
                  \    /
               bottom (non reachable)

   * 'semidet' = 0 or 1 solutions
   * 'multi' = 1 or more solutions
   * 'det' = 1 solution
   * 'fails' = 0 solutions

Example: sorted_insert/3
------------------------

In order to see these analyses in action, assume that our predicate
'sorted_insert/3' is defined without the cut.  If we analyze the program
with this modification:

Exercise 8 (Making predicates deterministic).  Modify the predicate to
make it deterministic:
     :- module(_, [sorted_insert/3], [assertions,regtypes]).

     :- regtype num_pair(P).
     num_pair((X, Y)) :- num(X), num(Y).

     :- regtype list_pair(L).
     list_pair([]).
     list_pair([X|Xs]) :-
         num_pair(X),
         list_pair(Xs).

     :- regtype list_pair1(L).
     list_pair1([X|Xs]) :-
        num_pair(X),
        list_pair(Xs).
     %! \begin{code}
     :- pred sorted_insert(A,B,C) : (list_pair(A), num_pair(B), var(C)) => list_pair1(C).

     sorted_insert([], X, [X]).
     sorted_insert([(X1,F1)|L1], (X,F), [(X,F), (X1,F1)|L1]) :- X =< X1.
     sorted_insert([P|L1], X, [P|L]) :- sorted_insert(L1, X, L).
     %! \end{code}
     %! \begin{opts}
     A,ana_det=nfdet,name=sorted_insert,filter=tpred_plus
     %! \end{opts}

the output includes the following assertions:

     %% %% :- check pred sorted_insert(A,B,C)
     %% %%    : ( list_pair(A), num_pair(B), var(C) )
     %% %%    => list_pair1(C).

     :- checked calls sorted_insert(A,B,C)
        : ( list_pair(A), num_pair(B), var(C) ).

     :- checked success sorted_insert(A,B,C)
        : ( list_pair(A), num_pair(B), var(C) )
        => list_pair1(C).

Thus, we can see that the analyzer does verify the assertion that we had
included.  However, we can also see these other assertions:

     :- true pred sorted_insert(A,B,C)
        : ( mshare([[C]]),
            var(C), ground([A,B]), list_pair(A), num_pair(B), term(C) )
        => ( ground([A,B,C]), list_pair(A), num_pair(B), list_pair1(C) )
        + ( multi, covered, possibly_not_mut_exclusive ).

     :- true pred sorted_insert(A,B,C)
        : ( mshare([[C]]),
            var(C), ground([A,B]), list_pair(A), num_pair(B), term(C) )
        => ( ground([A,B,C]), list_pair(A), num_pair(B), list_pair1(C) )
        + ( multi, covered, possibly_not_mut_exclusive ).

As we mentioned before, the '+' field in 'pred' assertions describes
properties of the computation of the predicate (such as determinism or
non-failure).  According to the diagram shown before, 'multi' states
that there is at least one solution but may have more.  Also, 'covered'
means that for any input there is at least one clause whose succeeds and
'possibly_not_mut_exclusive' denotes that mutual exclusion is not
ensured.  This is because when the first argument is a non-empty list
both the second and third clauses will succeed.  When reasoning about
determinacy, it is a necessary condition (but not sufficient) that
clauses of the predicate be pairwise mutually exclusive, i.e., that only
one clause will produce solutions.  In order to solve this, we can add
either the complementary 'X > X1' condition in the third clause or the
cut in the second clause.  Obviously, for any particular call only one
of the clauses 'X =< X1' or 'X > X1' will succeed.  Adding one of these
two options and analyzing the program again we can see that the
predicate is deterministic (modifying the previous example you can
observe this behavior).

Dynamic Bug Finding with CiaoPP's Testing Facilities
====================================================

The specification throughout our program so far is that the predicate
'powers/3' is called with a list of numbers as first argument, a number
'N' as second argument, and a free variable in the third argument.
However, the original specification states that the numbers are actually
non-negative integers.  It also states that the list produced on success
in the third argument is also a list of non-negative integers, and,
furthermore, that this list is in ascending order (i.e., sorted in
ascending order).

We can specify all this by first defining new properties as follows (we
use 'nnegint' from the 'Ciao' libraries):
     :- prop sorted/1.
     sorted([]).
     sorted([_]).
     sorted([X,Y|Ys]) :-
         X=<Y,
         sorted([Y|Ys]).

     :- prop list_nnegint(X) + regtype
     # "Verifies that @var{X} is list of non-negative integers." .
     list_nnegint([]).
     list_nnegint([X|T]) :-
         nnegint(X),
         list_nnegint(T).

'list_nnegint/1' checks if the argument is a list of non-negative
integers, 'sorted/1' checks if the argument is a sorted list.  Other
properties like 'var/1' or 'not_fails' are builtins, defined in
libraries.  These properties are important because they will be used by
'CiaoTest' as generators for test cases.  Then including them in our
program together with the following assertion:

     :- pred powers(A,B,C) : (list_nnegint(A), nnegint(B), var(C)) => (list_nnegint(C), sorted(C)) + not_fails.
and running 'CiaoPP' we will see that this assertion cannot be proved
nor disproved statically with the standard 'CiaoPP' domains:

     :- check success powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) )
        => ( list_nnegint(C), sorted(C) ).

     :- check comp powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) )
        + not_fails.

     :- checked calls powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) ).

This is because there is no abstract domain that covers properly the
'sorted/1' property.  This is something that can occur specially with
user-defined properties.  In these cases 'CiaoPP' will generate run-time
checks for the properties that have not been verified statically in such
assertions.  Such runtime checks will raise an error if the assertion is
violated, albeit at run time.  Thus, they at least ensure that execution
paths that violate the assertions are captured during execution.

Since letting errors be raised after deployment is less desirable, a
step that can be taken in order to deal with non-verified assertions is
to generate test cases to try to find a counterexample, i.e., an input
for which an error is raised by the run-time tests.  This can be done
either manually, by adding 'test' assertions (unit tests), to the
program, or using the provisions that 'CiaoPP' offers for automatically
generating test cases from the call fields of assertions.  This process
works as follows:

Consider this buggy implementation of 'quicksort/2' in 'powers/3':
     :- module(_,[powers/3],[assertions,nativeprops]).

     :- prop list_nnegint(X) + regtype  .
     list_nnegint([]).
     list_nnegint([X|T]) :-
         nnegint(X), list_nnegint(T).

     :- prop sorted(Xs).

     sorted([]).
     sorted([_]).
     sorted([X,Y|Ns]) :-
             X =< Y,
             sorted([Y|Ns]).

     %! \begin{focus}

     :- pred powers(A,B,C) : (list_nnegint(A), nnegint(B), var(C)) => (list_nnegint(C), sorted(C) ) + not_fails.

     :- test powers(A,B,C) : (A = [3,4,5], B = 17) => (C = [3,4,5,9,16,25,27,64,81,125,243,256,625,729,1024,2187,3125]) + not_fails.
     :- test powers(A,B,C) : (A = [2,9999999,9999998], B = 20) => (C = [2,4,8,16,32,64,128,256,512,1024,2048,4096,8192,16384,32768,65536,131072,262144,524288,1048576]) + not_fails.
     :- test powers(A,B,C) : (A = [2,4], B = 6) => (C = [2,4,8,16,32,64]) + not_fails.

     powers([],_,[]).
     powers(Factors,N,Powers) :-
         quicksort(Factors, SFactors),
         create_pairs(SFactors,Pairs),
         first_powers(N,Pairs,Powers).

     % qsort with a slight mistake: it may fail when there are repeated numbers in the list
     quicksort(Xs,Ys) :- qsort(Xs,Ys,[]).

     qsort([],DL,DL).

     qsort([X|Xs],Head,Tail) :-
         partition(Xs,X,L,R),
         qsort(L,Head,[X|QR]),
         qsort(R,QR,Tail).

     partition([],_,[],[]).
     partition([X|Xs],Pv,[X|L],R) :- X < Pv, !, partition(Xs,Pv,L,R). % (1) should be >= (or =< below)
     partition([X|Xs],Pv,L,[X|R]) :- X > Pv, partition(Xs,Pv,L,R).
     %! \end{focus}

     create_pairs([],[]).
     create_pairs([X|R],[(X,X)|S]) :- create_pairs(R,S).

     first_powers(N,[(Power,Factor)|PFs],[Power|Powers]) :-
         N > 0, !,
         N1 is N-1,
         remove_power(Power,PFs,PFs1),
         Power1 is Power*Factor,
         sorted_insert(PFs1,(Power1,Factor),PFs2),
         first_powers(N1,PFs2,Powers).
     first_powers(0,_,[]).

     remove_power(_,[],[]).
     remove_power(Power,[(Power1,Factor)|RestOut],[(Power1,Factor)|RestOut]) :-
         Power =\= Power1, !.
     remove_power(Power,[_|RestPFsIn],PFsOut) :-
         remove_power(Power,RestPFsIn,PFsOut).

     sorted_insert([], X, [X]).
     sorted_insert([(X1,F1)|L1], (X,F), [(X,F), (X1,F1)|L1]) :- X =< X1, !.
     sorted_insert([P|L1], X, [P|L]) :- sorted_insert(L1, X, L).
This predicate sorts a given list of integers from lowest to highest.
However, we have introduced an intentional bug '(1 in the listing)' that
causes the program to fail when a list with repeated elements is given.

After the 'pred' assertion we can see three test assertions that the
user has included to check the behavior of the predicate.  They cover
the examples given in the problem statement.

Setting up CiaoPP flags
-----------------------

In order to carry out the operations described above (running unit tests
and test generation) automatically we need to activate a few flags in
CiaoPP's menu.  Under the 'Test assertions' category, we will find the
'Run test assertions (run_utests)' and 'Generate tests from check
assertions (test_gen)' flags that we need to turn on:

[ciaopp_tutorials.cachedoc/texinfo/ciaopp-flag-menu_autofig]

Now, when we tell 'CiaoPP' to perform assertion checking, it will first
run the usual static analysis and checking of assertions, then it will
run all unit tests present in the program.  If at least one of them
fails, then random test generation is skipped.  However, if all unit
tests pass, test generation is performed as a last step to try to find
test cases that make the assertions fail, hence revealing faults in our
code.

Running unit tests
------------------

After assertion checking, 'CiaoTest' runs all unit tests present in the
program:

     :- checked test powers(A,B,C)
        : ( (A=[3,4,5]), (B=17) )
        => (C=[3,4,5,9,16,25,27,64,81,125,243,256,625,729,1024,2187,3125])
        + not_fails.

     :- checked test powers(A,B,C)
        : ( (A=[2,9999999,9999998]), (B=20) )
        => (C=[2,4,8,16,32,64,128,256,512,1024,2048,4096,8192,16384,32768,65536,131072,262144,524288,1048576])
        + not_fails.

     :- checked test powers(A,B,C)
        : ( (A=[2,4]), (B=6) )
        => (C=[2,4,8,16,32,64])
        + not_fails.

In this case all tests passed without errors, so random test generation
is performed.

Generating Tests
----------------

'CiaoTest' will read the assertions left to be checked and generate
goals for that predicate satisfying the assertion precondition and
execute them to either check that the assertion holds for those cases or
find errors.  Lets see what 'CiaoTest' did:

     ERROR: (lns 19-20) Failed test for predicate:
     power_testing_eterms_nf_shfr_co:powers(A,B,C).
     Test case:
             powers([72,72,92,95,58],13,_).
     In *comp*, unsatisfied property:
             not_fails.
     Where:
             fails

     ERROR: (lns 81-82) Failed in power_testing_eterms_nf_shfr_co:powers(A,B,C).

By default 'CiaoTest' generates 100 cases for each assertion, or stops
before if it finds one case that does not meet the assertion
post-condition.  Keep in mind that the generation is random, so do not
expect to get the same results if you try this yourself, in fact, it may
very well be that none of the test cases generated makes the program
fail, so it is recommended to run 'CiaoTest' a couple times or increase
the number of cases to be generated using the 'num_test_cases' option in
CiaoPP's flags menu.  For that same reason, it is also important to note
that of course even if 'CiaoTest' does not find any cases that violate
the assertion, one cannot affirm that the assertion is true.

The failed test cases that we got are valid calls to 'powers/3' that did
not comply with the post-condition, in particular, they violated the
computational properties field, since they where required to not fail.
Thus, they are counter-examples that prove that the remaining part of
the assertion does not hold.  Now we are aware that the predicate is not
behaving as it should.  If we look at the input lists that violate the
assertion, it is not too difficult too realize that there are repeated
elements in them, and that this may be the source of our problems.

If it is not apparent where the bug is through observation, a good next
step would be to debug the predicate in the interactive source debugger
calling it with the counter-examples that 'CiaoTest' generated for us
and look for the point in which the error occurs.

If we take a look into CiaoPP's output file now, we will see that some
of the assertions left to be checked after static analysis have been
proven false by the counter-examples found via test generation:

     :- check success powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) )
        => ( list_nnegint(C), sorted(C) ).

     :- checked calls powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) ).

     :- false comp powers(A,B,C)
        : ( list_nnegint(A), nnegint(B), var(C) )
        + ( not_fails, by((texec 4)) ).

     :- checked test powers(A,B,C)
        : ( (A=[3,4,5]), (B=17) )
        => (C=[3,4,5,9,16,25,27,64,81,125,243,256,625,729,1024,2187,3125])
        + not_fails.

     :- checked test powers(A,B,C)
        : ( (A=[2,9999999,9999998]), (B=20) )
        => (C=[2,4,8,16,32,64,128,256,512,1024,2048,4096,8192,16384,32768,65536,131072,262144,524288,1048576])
        + not_fails.

     :- checked test powers(A,B,C)
        : ( (A=[2,4]), (B=6) )
        => (C=[2,4,8,16,32,64])
        + not_fails.
In the computation properties field of the assertions that have been
marked as false, we can see a new property 'by/1' that is used to
indicate the source of the failure.  In our case, that source is the
failed test cases, which are represented by 'texec' declarations, each
identified by a different 'id/1', which is what appears in the 'by/1'
field.

In this section we showed how given a buggy program we can follow a
simple methodology to help us spot those bugs.  'CiaoPP''s analyzers and
verifiers offer us the static analysis tools to check part of the
assertions and then we can ask it to use 'CiaoTest' to check the
remaining unchecked assertions by running the unit tests present in the
program and with assertion-based random test generation.  Depending on
the properties involved, this procedure can often be fully automatic,
just needing setting the relevant flags.  If failing test cases are
found they can be excellent starting points for more classical
debugging.  Other possible approaches include implementing a new
abstract domain for a specific property (i.e., in this case a new domain
that infers if a list is sorted or not) or proving the property by hand
or with an automatic theorem prover.  These solutions are more powerful
than testing, in the sense that they can potentially verify that there
are no errors in the program, while testing can find bugs but cannot
verify that there are none, but they are also more involved.

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
     % 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).
The assertion for predicate 'partition/4' (twenty-third line) 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' expresses the
expected calling pattern, and that the call can have at most one answer,
property 'semidet'.

In the 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) ).

Program Development using the CiaoPP Program Processor
******************************************************

Author(s): The Ciao Development Team.

'CiaoPP' is a standalone preprocessor to the standard clause-level
compiler.  It performs source-to-source transformations.  The input to
'CiaoPP' are logic programs (optionally with assertions and syntactic
extensions).  The output are error/warning messages plus the transformed
logic program, with results of analysis (as assertions), results of
static checking of assertions, assertion run-time checking code, and
optimizations (specialization, parallelization, etc.).

This tutorial is organized as follows:

   * Getting Started gives the "getting started" basics.
   * Static Analysis and Program Assertions shows how 'CiaoPP'
     performs program analysis.
   * Program Debugging and Assertion Checking does the same for
     program debugging and validation.

Getting Started
===============

In order to follow these examples you need to either:

   * Install 'Ciao' on your computer, including the development
     environment (see Installation for more information).  This
     includes 'CiaoPP' (and 'LPdoc').  You can then access 'CiaoPP' from
     the Emacs interface or the command line.

   * Run '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>.

To follow this tutorial we recommend installing it as many of the
advanced features are not yet included in the playground.  The
instructions below use the Emacs interface.

A 'CiaoPP' session consists in the preprocessing of a file.  The session
is governed by a menu, where you can choose the kind of preprocessing
you want to be done to your file among several analyses and program
transformations available.  This tutorial shows how to customize the
preprocessing but some predefined preprocessing options are described in
CiaoPP at a glance.

Clicking on the icon [ciaopp_tutorials.cachedoc/texinfo/button-options-new_autofig] in the buffer containing the file to be
preprocessed displays the menu, which will look (depending on the
options available in the current 'CiaoPP' version) something like the
"Preprocessor Option Browser" shown in:

[ciaopp_tutorials.cachedoc/texinfo/naive-menu-new_autofig]

Except for the first line, which refers to selecting levels of
customization.  You can select analysis and assertion checking
('analyze_check') or program optimization ('optimize'), and you can
later combine the four kinds of preprocessing.  The relevant options for
the 'action' selected are then shown, together with the relevant flags.

A description of the values for each option will be given as it is used
in the corresponding section of this tutorial.

Static Analysis and Program Assertions
======================================

The fundamental functionality behind 'CiaoPP' is static global program
analysis, based on abstract interpretation.  For this task 'CiaoPP' uses
the PLAI abstract interpreter [ MH92, BGH99].

The system infers information on variable-level properties such as moded
types, definiteness, freeness, independence, and grounding dependencies:
essentially, precise data structure shape and pointer sharing.  It can
also infer bounds on data structure sizes, as well as procedure-level
properties such as determinacy, termination, non-failure, and bounds on
resource consumption (time or space cost).  'CiaoPP' implements several
techniques for dealing with "difficult" language features (such as
side-effects, meta-programming, higher-order, etc.)  and as a result can
for example deal safely with arbitrary ISO-Prolog programs [ BCHP96].  A
unified language of assertions [ BCHP96, PBH00b] is used to express the
results of analysis, to provide input to the analyzer of program
specifications for debugging and validation, as well as the results of
the comparisons performed against the specifications.

Static Analysis Basics
----------------------

Consider the program defining a module which exports the 'qsort'
predicate:

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

     :- pred qsort(A,B) : (list(num, A), var(B)).

     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([],X,X).
     append([H|X],Y,[H|Z]):- append(X,Y,Z).
We have added a 'pred' assertion for the exported predicate 'qsort'
expressing that it should be called with its first argument bound to a
list of numbers.

Note the use of builtin properties (i.e., defined in modules which are
loaded by default, such as 'var', 'num', 'list', etc.).  Note also that
properties natively understood by different analysis domains can be
combined in the same assertion.

The sharing and freeness analysis abstract domain computes freeness,
independence, and grounding dependencies between program variables.

It is performed by selecting the menu option 'Aliasing-Mode':

[ciaopp_tutorials.cachedoc/texinfo/analysis-shfr-new_autofig]

The output of the analysis is performed via assertions (see Using assertions for preprocessing programs
for a detailed description).  In
this case three assertions appear:

     :- true pred qsort(A,B)
        : ( mshare([[B]]),
            var(B), ground([A]) )
        => ground([A,B]).

     :- true pred partition(_A,_1,Y1,Y2)
        : ( mshare([[Y1],[Y2]]),
            var(Y1), var(Y2), ground([_A,_1]) )
        => ground([_A,_1,Y1,Y2]).

     :- true pred append(_A,X,_B)
        : ( mshare([[_B]]),
            var(_B), ground([_A,X]) )
        => ground([_A,X,_B]).

These assertions express, for example, that the third and fourth
arguments of 'partition' have "output mode": when 'partition' is called
(':') 'Y1' and 'Y2' are free unaliased variables and they are ground on
success ('=>').  Also, 'append' is used in a mode in which the first and
second argument are input (i.e., ground on call).

Type Analysis
-------------

'CiaoPP' can infer (parametric) types for programs both at the predicate
level and at the literal level [ GdW94, GP02, VB02].  Different type
domains can be selected with the menu option 'Shape-Type' Analysis.  As
shown in the following screenshot:

[ciaopp_tutorials.cachedoc/texinfo/analysis-eterms-new_autofig]

At the predicate level the inferred information is:

     :- true pred qsort(A,B)
        : ( list(num,A), term(B) )
        => ( list(num,A), list(num,B) ).

     :- true pred partition(_A,_1,Y1,Y2)
        : ( list(num,_A), num(_1), term(Y1), term(Y2) )
        => ( list(num,_A), num(_1), list(num,Y1), list(num,Y2) ).

     :- true pred append(_A,X,_B)
        : ( list(num,_A), list1(num,X), term(_B) )
        => ( list(num,_A), list1(num,X), list1(num,_B) ).

where 'term' is any term and prop 'list' and 'list1' are defined in
'library(lists)' as:
     :- regtype list(T,L) #"@var{L} is a list of @var{T}'s.".
     :- meta_predicate list(pred(1),?).
     list(_T,[]).
     list(T,[X|L]) :- T(X), list(T,L).

     :- regtype list1(T,X) # "@var{X} is a list of @var{Y}s of at least one element.".
     :- meta_predicate list1(pred(1),?).
     list1(T,[X|R]) :- T(X), list(T,R).

Non-failure and Determinacy Analysis:
-------------------------------------

'CiaoPP' includes a non-failure analysis, based on [ DLGH97] and [
BLGH04], which can detect procedures and goals that can be guaranteed
not to fail, i.e., to produce at least one solution or not terminate.
It also can detect predicates that are "covered", i.e., such that for
any input (included in the calling type of the predicate), there is at
least one clause whose "test" (head unification and body builtins)
succeeds.  'CiaoPP' also includes a determinacy analysis based on [
LGBH05], which can detect predicates which produce at most one solution,
or predicates whose clause tests are mutually exclusive, even if they
are not deterministic (because they call other predicates that can
produce more than one solution).  Programs can be analyzed with this
kind of domains by selecting to perform 'Non-Failure' Analysis with
domain 'nf':

[ciaopp_tutorials.cachedoc/texinfo/analysis-nf-new_autofig]

Analyzing qsort with the 'nf' domain will produce (among others) the
following assertion:

     :- true pred qsort(A,B)
        : ( mshare([[B]]),
            var(B), ground([A]), list(num,A), term(B) )
        => ( ground([A,B]), list(num,A), list(num,B) )
        + ( not_fails, covered ).

     :- true pred qsort(A,B)
        : ( mshare([[B]]),
            var(B), ground([A]), list(num,A), term(B) )
        => ( ground([A,B]), list(num,A), list(num,B) )
        + ( not_fails, covered ).

The '+' field in 'pred' assertions can contain a conjunction of global
properties of the computation of the predicate.  'not_fails' states that
if the precondition is met, the predicate will never fail.

Size, Resources, and Termination Analysis
-----------------------------------------

'CiaoPP' can also infer lower and upper bounds on the sizes of terms and
the computational cost of predicates [ DLGHL94, DLGHL97].  The cost
bounds are expressed as functions on the sizes of the input arguments
and yield the number of resolution steps.  Various measures are used for
the "size" of an input, such as list-length, term-size, term-depth,
integer-value, etc.  Note that obtaining a non-infinite upper bound on
cost also implies proving termination of the predicate.

Our resource analysis is parametric on the resources, therefore a
package defining the resource to be used has to be imported in the
module, in this case we use the default package that infers information
about computation al steps.  This is done by replacing the first line
by:

     :- module(qsort, [qsort/2], [assertions,predefres(res_steps)]).
Also, to be able to infer lower bounds a non-failure and determinacy
analysis has to be performed:

[ciaopp_tutorials.cachedoc/texinfo/analysis-resources-new_autofig]

As an example, the following assertions are part of the output of the
upper bounds analysis:

     :- true pred qsort(A,B)
        : ( list(num,A), var(B) )
        => ( list(num,A), list(num,B),
             size(ub,length,B,2**length(A)-1.0) )
        + cost(ub,steps,sum($(j),1,length(A),$(j)*2**(length(A)- $(j)))+2.0*2**length(A)+length(A)*2**(length(A)-1)-1.0).

     :- true pred append(_A,X,_B)
        : ( list(num,_A), list1(num,X), var(_B) )
        => ( list(num,_A), list1(num,X), list1(num,_B),
             size(ub,length,_B,length(X)+length(_A)) )
        + cost(ub,steps,length(_A)+1).

For example, the second assertion is inferring on success
'size(ub,length,B,length(X)+length(A))', which means that an (upper)
bound on the size of the third argument of 'append/3' is the sum of the
sizes of the first and second arguments.  The inferred upper bound on
computational steps ('+ cost(ub,steps,length(_A)+1)') is the length of
the first argument of 'append/3'.

The following is the output of the lower-bounds analysis:

     :- true pred qsort(A,B)
        : ( list(num,A), var(B) )
        => ( list(num,A), list(num,B),
             size(lb,length,B,1) )
        + cost(lb,steps,0).

     :- true pred append(_A,X,_B)
        : ( list(num,_A), list1(num,X), var(_B) )
        => ( list(num,_A), list1(num,X), list1(num,_B),
             size(lb,length,_B,length(X)+length(_A)) )
        + cost(lb,steps,0).

The lower-bounds analysis uses information from the non-failure
analysis, without which a trivial lower bound of 0 would be derived.

In this case it is inferred that on success the lower bound of the third
argument of append is size(lb,length,_B,length(X)+length(_A)) (the same
as the upper bound!), and the upper bound on computational steps '+
cost(lb,steps,0)', which represents the case in which the first list to
concatenate is empty.

Decidability, Approximations, and Safety
----------------------------------------

As a final note on the analyses, it should be pointed out that since
most of the inferred properties are in general undecidable at
compile-time, the inference technique used, abstract interpretation, is
necessarily approximate, i.e., possibly imprecise.  On the other hand,
such approximations are also always guaranteed to be safe, in the sense
that (modulo bugs, of course) they are never incorrect: the properties
stated in inferred assertions do always hold of the program.

Program Debugging and Assertion Checking
========================================

'CiaoPP' is also capable of static assertion checking, and debugging
using the ideas outlined so far.  To this end, it implements the
framework described in [ HPB99, PBH00a] which involves several of the
tools which comprise 'CiaoPP'.  The following figure depicts the overall
architecture.

[ciaopp_tutorials.cachedoc/texinfo/ciaopp-framework_autofig]

Hexagons represent the different tools involved and arrows indicate the
communication paths among them.

Program verification and detection of errors is first performed at
compile-time by inferring properties of the program via abstract
interpretation-based static analysis and comparing this information
against (partial) specifications written in terms of assertions (see [
HPBLG05] for a detailed description of the sufficient conditions used
for achieving this 'CiaoPP' functionality).

The static checking is provably safe in the sense that all errors
flagged are definite violations of the specifications.

Assertions and Properties
-------------------------

As introduced before, assertions are a means of specifying properties
which are (or should be) true of a given predicate, predicate argument,
and/or program point.  See Using assertions for preprocessing programs
for a more detailed description, of the concepts that we
briefly introduce now.

They are of the form ':- [Status] Scope Head : Pre => Post + Comp.',
where 'Status' is a qualifier of the meaning of the assertion, 'Scope'
describes where the assertion is applied, 'Head' is a normalized atom,
and 'Pre', 'Post', and 'Comp' are conjunctions of properties.

So far we have seen assertions with 'Status' 'true', which mean that
they express the behavior inferred by the analyzer.  This status can
only appear in the output of the analyzer (i.e.  the user should not use
it).

   * 'check': (input and output status) default status (i.e., if no
     status is specified), expresses properties that the user wants
     ensured to hold at run-time, i.e., that the analyzer should prove
     (or else generate run-time checks for).
   * 'trust': (input status) the assertion represents an actual behavior
     of the predicate that the analyzer may not be able to infer
     automatically.
   * 'checked': (output status) the assertion was proved to hold
     statically by the analyzer.
   * 'false': (output status) the assertion was proved not to hold
     statically by the analyzer.

In 'CiaoPP' properties are predicates, which may be builtin or user
defined.  For example, the property 'var' used in the above examples is
the standard builtin predicate to check for a free variable.  The same
applies to 'ground' and 'mshare'.  The properties used by an analysis in
its output (such as 'var', 'ground', and 'mshare' for the previous mode
analysis) are said to be native for that particular analysis.  The
system requires that properties be marked as such with a 'prop'
declaration which must be visible to the module in which the property is
used.

Properties declared and/or defined in a module can be exported as any
other predicate.  For example:
     :- prop list/1.
     list([]).
     list([_|L]) :- list(L).
or, using the functional syntax package, more compactly as:
     :- prop list/1. list := [] | [_|list].
defines the property 'list'.  A list is an instance of a very useful
class of user-defined properties called regular types [ YS87, DZ92,
GdW94, GP02, VB02], which herein are simply a syntactically restricted
class of logic programs.  We can mark this fact by stating ':- regtype
list/1.' instead of ':- prop list/1.' (this can be done automatically).
The definition above can be included in a user program or,
alternatively, it can be imported from a system library, e.g.: ':-
use_module(library(lists),[list/1]).'

Using analysis information for debugging
----------------------------------------

The idea of using analysis information for debugging comes naturally
after observing analysis outputs for erroneous programs.  Consider this
buggy implementation of 'qsort':

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

     :- pred qsort(A,B) : (list(num, A), var(B)).

     qsort([],[]).
     qsort([First|Rest],Result) :-
         partition(Rest,First,Sm,Lg),
         qsort(Sm,SmS), qsort(Lg,LgS),
         append(SmS,[x|LgS],Result).  % <-- 'x' should be X (variable)

     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([],X,X).
     append([H|X],Y,[H|Z]):- append(X,Y,Z).
The result of regular type analysis for this program includes the
following code:

     :- true pred qsort(A,B)
        : ( term(A), term(B) )
        => ( list(num,A), list(^(x),B) ).

where 'list(^x,B)' means "B is a list of atoms 'x'.".  The information
inferred does not seem compatible with a correct definition of 'qsort',
which clearly points to a bug in the program.

Static Checking of Assertions in System Libraries
-------------------------------------------------

In addition to manual inspection of the analyzer output, 'CiaoPP'
includes a number of automated facilities to help in the debugging task.
For example, 'CiaoPP' can find incompatibilities between the ways in
which library predicates are called and their intended mode of use,
expressed in the form of assertions in the libraries themselves.  Also,
the preprocessor can detect inconsistencies in the program and check the
assertions present in other modules used by the program.

Consider a different implementation of 'qsort', also with bugs:

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

     :- pred qsort(A,B) : (list(num, A), var(B)).

     qsort([X|L],R) :-
         partition(L,L1,X,L2),         % <-- swapped second and third arguments
         qsort(L2,R2), qsort(L1,R1),
         append(R2,[X|R1],R).
     qsort([],[]).

     partition([],_B,[],[]).
     partition([e|R],C,[E|Left1],Right):-  % <-- 'e' should be E (variable)
         E < C, !, partition(R,C,Left1,Right).
     partition([E|R],C,Left,[E|Right1]):-
         E >= C, partition(R,C,Left,Right1).

     append([],X,X).
     append([H|X],Y,[H|Z]):- append(X,Y,Z).
By default, the option Static assertion checking is set to on, which
means that the system will automatically detect the analyses to be
performed in order to check the program, depending on the information
available in the program assertions (in the example in the pred
assertion informs how the predicate 'qsort/2' will be called using types
and modes information only).

Using the default options, and running 'CiaoPP', we obtain the following
messages (and the system highlights the line which produces the first of
them), as shown:

     WARNING (preproc_errors): (lns 4-8) goal bugqsort2:partition(L,L1,X,L2) at literal 1 does not succeed!

     WARNING (ctchecks_pp_messages): (lns 12-13) the head of clause 'bugqsort2:partition/4/2' is incompatible with its call type
          Head:      bugqsort2:partition([e|R],C,[E|Left1],Right)
          Call Type: bugqsort2:partition(basic_props:list(num),term,num,term)

     WARNING (preproc_errors): (lns 14-15) goal arithmetic:>=(E,C) at literal 1 does not succeed!

     ERROR (ctchecks_pp_messages): (lns 14-15) At literal 1 false assertion:
     :- check calls B>=A
        : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
     because on call arithmetic:>=(A,B) :

     [shfr] native_props:mshare([[B],[_],[A],[_],[A]]),term_typing:var(B),term_typing:var(A)

First and the last two messages warn that all calls to 'partition' and
'>=/2' will fail, something normally not intended (e.g., in our case).
The error message indicates a wrong call to a builtin predicate, which
is an obvious error.  This error has been detected by comparing the mode
information obtained by global analysis, which at the corresponding
program point indicates that the second argument to the call to '>=/2'
is a variable, with the assertion:

     :- check calls B>=A
        : ( nonvar(B), nonvar(A), arithexpression(B), arithexpression(A) ).
which is present in the default builtins module, and which implies that
the two arguments to '>=/2' should be ground when this arithmetic
predicate is called.  The message signals a compile-time, or abstract,
incorrectness symptom [ BDD97], indicating that the program does not
satisfy the specification given (that of the builtin predicates, in this
case).  Checking the indicated call to 'partition' and inspecting its
arguments we detect that in the definition of 'qsort', 'partition' is
called with the second and third arguments in reversed order - the
correct call is 'partition(L,X,L1,L2)'.

After correcting this bug, we proceed to perform another round of
compile-time checking, which continues producing the following message:

     WARNING (ctchecks_pp_messages): (lns 12-13) the head of clause 'bugqsort3:partition/4/2' is incompatible with its call type
          Head:      bugqsort3:partition([e|R],C,[E|Left1],Right)
          Call Type: bugqsort3:partition(basic_props:list(num),num,term,term)

This time the error is in the second clause of 'partition'.  Checking
this clause we see that in the first argument of the head there is an
'e' which should be 'E' instead.  Compile-time checking of the program
with this bug corrected does not produce any further warning or error
messages.

Static Checking of User Assertions and Program Validation
---------------------------------------------------------

Though, as seen above, it is often possible to detect error without
adding assertions to user programs, if the program is not correct, the
more assertions are present in the program the more likely it is for
errors to be automatically detected.  Thus, for those parts of the
program which are potentially buggy or for parts whose correctness is
crucial, the programmer may decide to invest more time in writing
assertions than for other parts of the program which are more stable.
In order to be more confident about our program, we add to it the
following 'check' assertions (the 'check' prefix is assumed when no
prefix is given, as in the example shown):

     :- pred qsort(A,B) : (list(num, A), var(B)).

     qsort([X|L],R) :-
         partition(L,L1,X,L2),
         qsort(L2,R2), qsort(L1,R1),
         append(R2,[x|R1],R).
     qsort([],[]).

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

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

     :- calls   qsort(A,B)         : list(num, A).                     % A1
     :- success qsort(A,B)         => (ground(B), sorted_num_list(B)). % A2
     :- calls   partition(A,B,C,D) : (ground(A), ground(B)).           % A3
     :- success partition(A,B,C,D) => (list(num, C),ground(D)).        % A4
     :- calls   append(A,B,C)      : (list(num,A),list(num,B)).        % A5
     :- comp    partition/4        + not_fails.                        % A6
     :- comp    partition/4        + is_det.                           % A7
     :- comp    partition(A,B,C,D) + terminates.                       % A8

     :- prop 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]).
where we also use a new property, 'sorted_num_list', defined in the
module itself.  These assertions provide a partial specification of the
program.  They can be seen as integrity constraints: if their properties
do not hold at the corresponding program points (procedure call,
procedure exit, etc.), the program is incorrect.  'Calls' assertions
specify properties of all calls to a predicate, while 'success'
assertions specify properties of exit points for all calls to a
predicate.  Properties of successes can be restricted to apply only to
calls satisfying certain properties upon entry by adding a ':' field to
'success' assertions.  Finally, 'Comp' assertions specify global
properties of the execution of a predicate.  These include complex
properties such as determinacy or termination and are in general not
amenable to run-time checking.  They can also be restricted to a subset
of the calls using ':'.  More details on the assertion language can be
found in [ PBH00b].

'CiaoPP' can perform compile-time checking of the assertions above, by
comparing them with the assertions inferred by analysis (see [ HPBLG05,
BDD97, PBH00c] for details), producing as output the following
assertions:

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

     :- check success qsort(A,B)
        => sorted_num_list(B).

     :- checked calls partition(A,B,C,D)
        : ( ground(A), ground(B) ).

     :- checked success partition(A,B,C,D)
        => ( list(num,C), ground(D) ).

     :- checked comp partition(_A,_B,_C,_D)
        + not_fails.

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

     :- checked comp partition(A,B,C,D)
        + terminates.

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

In order to produce this output, the 'CiaoPP' menu must be set to the
same options as those used for checking assertions in system libraries.
Since the on mode has been used for the option Static assertion
checking, 'CiaoPP' has automatically detected that the program must be
analyzed not only for types and modes domains, but also to check
non-failure, determinism, and upper-bound cost.  Note that a number of
initial assertions have been marked as 'checked', i.e., they have been
validated.  If all assertions had been moved to this 'checked' status,
the program would have been verified.  In these cases 'CiaoPP' is
capable of generating certificates which can be checked efficiently for,
e.g., mobile code applications [ APH04].  However, in our case assertion
'A5' has not been verified.  This indicates a violation of the
specification given, which is also flagged by 'CiaoPP' as follows:

     WARNING (ctchecks_pp_messages): (lns 18-18) the head of clause 'bugqsort_assertions:append/3/2' is incompatible with its call type
          Head:      bugqsort_assertions:append([H|X],Y,[H|Z])
          Call Type: bugqsort_assertions:append([],[^(x)],term)

The error is now in the call 'append(R2,[x|R1],R)' in 'qsort' ('x'
instead of 'X').  Assertions 'A1', 'A3', 'A4', 'A6', 'A7', and 'A8' have
been detected to hold.  Note that though the predicate 'partition' may
fail in general, in the context of the current program it can be proved
not to fail (assertion 'A6').  However, it was not possible to prove
statically assertion also 'A2', which has remained with 'check' status.
Note also that 'A2' has been simplified, and this is because the mode
analysis has determined that on success the second argument of 'qsort'
is ground, and thus this does not have to be checked at run-time.  On
the other hand the analyses used in our session (types, modes,
non-failure, determinism, and upper-bound cost analysis) do not provide
enough information to prove that the output of 'qsort' is a sorted list
of numbers, since this is not a native property of the analyses being
used.  While this property could be captured by including a more refined
domain (such as constrained types), it is interesting to see what
happens with the analyses selected for the example.

(1)

Performance Debugging and Validation:
-------------------------------------

'CiaoPP' allows stating assertions about the efficiency of the program.
This is done by stating lower and/or upper bounds on the computational
cost of predicates (given in number of execution steps).  Consider for
example the naive reverse program:

     :- module(_, [nrev/2], [assertions,predefres(res_steps)]).

     :- use_module(library(assertions/native_props)).

     :- pred nrev(A,B) : (ground(A), list(A), var(B)).
     %:- check comp nrev(A,B) + steps_ub(length(A)+1).     % (1) false
     %:- check comp nrev(A,B) + steps_o(length(A)).        % (2) false
     %:- check comp nrev(A,B) + steps_o(exp(length(A),2)). % (3) checked

     nrev([],[]).
     nrev([H|L],R) :-
         nrev(L,R1),
         append(R1,[H],R).

     append([],Ys,Ys).
     append([X|Xs],Ys,[X|Zs]):- append(Xs,Ys,Zs).
Suppose that the programmer thinks that the cost of 'nrev' is given by a
linear function on the size (list-length) of its first argument, maybe
because he has not taken into account the cost of the 'append' call, and
adds the assertion:

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

     :- use_module(library(assertions/native_props)).

     :- pred nrev(A,B) : (ground(A), list(A), var(B)).
     %! \begin{focus}
     :- check comp nrev(A,B) + steps_ub(length(A)+1).

     nrev([],[]).
     nrev([H|L],R) :-
         nrev(L,R1),
         append(R1,[H],R).

     append([],Ys,Ys).
     append([X|Xs],Ys,[X|Zs]):- append(Xs,Ys,Zs).
     %! \end{focus}
Since 'append' is linear, it causes 'nrev' to be quadratic.  'CiaoPP'
can be used to inform the programmer about this false idea about the
cost of 'nrev'.

As before, we set the option 'Action' to 'analyze_check' in the menu.
We get the following error message:

     ERROR (ctchecks_pred_messages): (lns 6-6) False assertion:
     :- check comp nrev(A,B)
        + steps_ub(length(A)+1).
     because the comp field is incompatible with inferred comp:
     [generic_comp] covered,is_det,mut_exclusive,not_fails,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)

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

This message states that 'nrev' will take at least '0.5*(length(A))^2 +
1.5*length(A) + 1' resolution steps (which is the cost analysis output),
while the assertion requires that it take at most 'length(A)+1'
resolution steps.  The cost function in the user-provided assertion is
compared with the lower-bound cost assertion inferred by analysis.  This
allows detecting the inconsistency and proving that the program does not
satisfy the efficiency requirements imposed.  Upper-bound cost
assertions can also be proved to hold, i.e., can be 'checked', by using
upper-bound cost analysis rather than lower-bound cost analysis.  In
such case, it holds when the upper-bound computed by analysis is lower
or equal than the upper-bound stated by the user in the assertion.  The
converse holds for lower-bound cost assertions.

'CiaoPP' can also verify or falsify cost assertions expressing worst
case computational complexity orders (this is specially useful if the
programmer does not want or does not know which particular cost function
should be checked).  For example, suppose now that the programmer adds
the following "check" assertion:

     :- check comp nrev(A,B) + steps_o(length(A)).
In this case, we get the following error message:

     ERROR (ctchecks_pred_messages): (lns 6-6) False assertion:
     :- check comp nrev(A,B)
        + steps_o(length(A)).
     because the comp field is incompatible with inferred comp:
     [generic_comp] covered,is_det,mut_exclusive,not_fails,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)

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

This message states that 'nrev' will take at least '0.5(length(A))^2 +
1.5length(A) + 1' resolution steps (which is the cost analysis output,
as in the previous example), while the assertion requires that the worst
case cost of 'nrev' be linear on 'length(A)' (the size of the input
argument).

If the programmer adds now the following "check" assertion:

     :- check comp nrev(A,B) + steps_o(exp(length(A),2)).
which states that the worst case cost of 'nrev' is quadratic, i.e.  is
in , where is the length of the first list (represented as 'length(A)').
Then the assertion is validated and the following "checked" assertion is
included in the output produced by 'CiaoPP':

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

     :- checked comp nrev(A,B)
        + steps_o(exp(length(A),2)).

'CiaoPP' can certify programs with resource consumption assurances [
HALGP04].

   ---------- Footnotes ----------

   (1) Note that while property 'sorted_num_list' cannot be proved with
only (over approximations) of mode and regular type information, it may
be possible to prove that it does not hold (an example of how properties
which are not natively understood by the analysis can also be useful for
detecting bugs at compile-time): while the regular type analysis cannot
capture perfectly the property 'sorted_num_list', it can still
approximate it (by analyzing the definition) as 'list(num, B)'.  If type
analysis for the program were to generate a type for 'B' not compatible
with 'list(num, B)', then a definite error symptom would be detected.

References
**********

[APH04]
     E. Albert, G. Puebla, and M. V. Hermenegildo.
     An Abstract Interpretation-based Approach to Mobile Code Safety.
     In Proc.  of Compiler Optimization meets Compiler Verification
     (COCV'04), Electronic Notes in Theoretical Computer Science 132(1),
     pages 113-129.  Elsevier - North Holland, April 2004.

[BCHP96]
     F. Bueno, D. Cabeza, M. V. Hermenegildo, and G. Puebla.
     Global Analysis of Standard Prolog Programs.
     In European Symposium on Programming, number 1058 in LNCS, pages
     108-124, Sweden, April 1996.  Springer-Verlag.

[BDD97]
     F. Bueno, P. Deransart, W. Drabent, G. Ferrand, M. V. Hermenegildo,
     J. Maluszynski, and G. Puebla.
     On the Role of Semantic Approximations in Validation and Diagnosis
     of Constraint Logic Programs.
     In Proc.  of the 3rd.  Int'l Workshop on Automated
     Debugging-AADEBUG'97, pages 155-170, Linköping, Sweden, May 1997.
     U. of Linköping Press.

[BGH99]
     F. Bueno, M. García de la Banda, and M. V. Hermenegildo.
     Effectiveness of Abstract Interpretation in Automatic
     Parallelization: A Case Study in Logic Programming.
     ACM Transactions on Programming Languages and Systems,
     21(2):189-238, March 1999.

[BLGH04]
     F. Bueno, P. López-García, and M. V. Hermenegildo.
     Multivariant Non-Failure Analysis via Standard Abstract
     Interpretation.
     In 7th International Symposium on Functional and Logic Programming
     (FLOPS 2004), number 2998 in LNCS, pages 100-116, Heidelberg,
     Germany, April 2004.  Springer-Verlag.

[DLGH97]
     S.K. Debray, P. López-García, and M. V. Hermenegildo.
     Non-Failure Analysis for Logic Programs.
     In 1997 International Conference on Logic Programming, pages 48-62,
     Cambridge, MA, June 1997.  MIT Press, Cambridge, MA.

[DLGHL94]
     S.K. Debray, P. López-García, M. V. Hermenegildo, and N.-W. Lin.
     Estimating the Computational Cost of Logic Programs.
     In Static Analysis Symposium, SAS'94, number 864 in LNCS, pages
     255-265, Namur, Belgium, September 1994.  Springer-Verlag.

[DLGHL97]
     S. K. Debray, P. López-García, M. V. Hermenegildo, and N.-W. Lin.
     Lower Bound Cost Estimation for Logic Programs.
     In 1997 International Logic Programming Symposium, pages 291-305.
     MIT Press, Cambridge, MA, October 1997.

[DZ92]
     P.W. Dart and J. Zobel.
     A Regular Type Language for Logic Programs.
     In Types in Logic Programming, pages 157-187.  MIT Press, 1992.

[GdW94]
     J.P. Gallagher and D.A. de Waal.
     Fast and Precise Regular Approximations of Logic Programs.
     In Pascal Van Hentenryck, editor, Proc.  of the 11th International
     Conference on Logic Programming (ICLP'94), pages 599-613.  MIT
     Press, 1994.

[GP02]
     J. Gallagher and G. Puebla.
     Abstract Interpretation over Non-Deterministic Finite Tree Automata
     for Set-Based Analysis of Logic Programs.
     In Fourth International Symposium on Practical Aspects of
     Declarative Languages, number 2257 in LNCS, pages 243-261.
     Springer-Verlag, January 2002.

[HALGP04]
     M. V. Hermenegildo, E. Albert, P. López-García, and G. Puebla.
     Some Techniques for Automated, Resource-Aware Distributed and
     Mobile Computing in a Multi-Paradigm Programming System.
     In Proc.  of EURO-PAR 2004, number 3149 in LNCS, pages 21-37.
     Springer-Verlag, August 2004.

[HPB99]
     M. V. Hermenegildo, G. Puebla, and F. Bueno.
     Using Global Analysis, Partial Specifications, and an Extensible
     Assertion Language for Program Validation and Debugging.
     In K. R. Apt, V. Marek, M. Truszczynski, and D. S. Warren, editors,
     The Logic Programming Paradigm: a 25-Year Perspective, pages
     161-192.  Springer-Verlag, July 1999.

[HPBLG05]
     M. V. Hermenegildo, G. Puebla, F. Bueno, and P. Lopez-Garcia.
     Integrated Program Debugging, Verification, and Optimization Using
     Abstract Interpretation (and The Ciao System Preprocessor).
     Science of Computer Programming, 58(1-2):115-140, October 2005.

[LGBH05]
     P. López-García, F. Bueno, and M. V. Hermenegildo.
     Determinacy Analysis for Logic Programs Using Mode and Type
     Information.
     In Proceedings of the 14th International Symposium on Logic-based
     Program Synthesis and Transformation (LOPSTR'04), number 3573 in
     LNCS, pages 19-35.  Springer-Verlag, August 2005.

[MH92]
     K. Muthukumar and M. Hermenegildo.
     Compile-time Derivation of Variable Dependency Using Abstract
     Interpretation.
     Journal of Logic Programming, 13(2/3):315-347, July 1992.

[PBH00a]
     G. Puebla, F. Bueno, and M. V. Hermenegildo.
     A Generic Preprocessor for Program Validation and Debugging.
     In P. Deransart, M. V. Hermenegildo, and J. Maluszynski, editors,
     Analysis and Visualization Tools for Constraint Programming, number
     1870 in LNCS, pages 63-107.  Springer-Verlag, September 2000.

[PBH00b]
     G. Puebla, F. Bueno, and M. V. Hermenegildo.
     An Assertion Language for Constraint Logic Programs.
     In P. Deransart, M. V. Hermenegildo, and J. Maluszynski, editors,
     Analysis and Visualization Tools for Constraint Programming, number
     1870 in LNCS, pages 23-61.  Springer-Verlag, September 2000.

[PBH00c]
     G. Puebla, F. Bueno, and M. V. Hermenegildo.
     Combined Static and Dynamic Assertion-Based Debugging of Constraint
     Logic Programs.
     In Logic-based Program Synthesis and Transformation (LOPSTR'99),
     number 1817 in LNCS, pages 273-292.  Springer-Verlag, March 2000.

[VB02]
     C. Vaucheret and F. Bueno.
     More Precise yet Efficient Type Inference for Logic Programs.
     In 9th International Static Analysis Symposium (SAS'02), volume
     2477 of Lecture Notes in Computer Science, pages 102-116.
     Springer-Verlag, September 2002.

[YS87]
     E. Yardeni and E. Shapiro.
     A Type System for Logic Programs.
     Concurrent Prolog: Collected Papers, pages 211-244, 1987.

Predicate Index
***************

Property Index
**************

Regular Type Index
******************

Declaration Index
*****************

Global Index
************

This is a global index containing pointers to places where concepts,
predicates, modes, properties, types, applications, authors, etc., are
referred to in the text of the document.