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