The CiaoPP Program Processor

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.

Note: This is the CiaoPP reference manual. To begin using CiaoPP, we suggest you start by following one or more of the companion CiaoPP tutorials available in the Ciao system documentation.

This documentation corresponds to version 1.7 (2023/7/13).