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 some basics about how CiaoPP works. It is however 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
- Static Analysis and Program Assertions
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 (see below for other languages). These tasks include:
- Inference of properties of the predicates and literals of the program, including Types, modes (Groundness and sharing), Term structure, and other variable instantiation properties, non-failure, determinacy, bounds on computational cost (e.g., Number of resolution steps of the computation), bounds on size of terms in the program, etc (see Available abstract domains).
- 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.
Support for other languages: CiaoPP is also used to develop analyzers and verifiers for other languages, and tools of different levels of maturity have been built for e.g., Java, (X)C, machine code, smart contracts (Michelson), etc. This is generally done using front ends that translate into the CiaoPP IR (Horn clauses). Some of these front-ends and extensions can be found in separate bundles.