ciaopp-tutorial

A Tutorial on Program Development and Optimizationusing the Ciao PreprocessorThe CiaoPP Development TeamJanuary 12, 2006AbstractWe present in a tutorial fashion CiaoPP, the preprocessor of the Ciao multi paradigmprogramming system, which implements a novel program development framework whichuses abstract interpretation as a fundamental tool. The framework uses modular, incrementalabstract interpretation to obtain information about the program. This information is usedto validate programs, to detect bugs with respect to partial specifications written using as sertions (in the program itself and/or in system libraries), to generate and simplify run timetests, and to perform high level program transformations such as multiple abstract special ization, parallelization, and resource usage control, all in a provably correct way. In the caseof validation and debugging, the assertions can refer to a variety of program points suchas procedure entry, procedure exit, points within procedures, or global computations. Thesystem can reason with much richer information than, for example, traditional types. Thisincludes data structure shape (including pointer sharing), bounds on data structure sizes,and other operational variable instantiation properties, as well as procedure level propertiessuch as determinacy, termination, non failure, and bounds on resource consumption (time orspace cost).1 IntroductionWe describe in a tutorial fashion CiaoPP, an implementation of ...