Automated Behavioural Verification of Prolog Programs
Baudouin Le Charlier, Christophe Leclère, Sabina Rossi, Agostino Cortesi · 1997
Although Prolog is still the most widely used logic language, it suffers from a number of drawbacks which prevent it from being truely declarative. Several authors have proposed methodologies to reconcile declarative programming with the algorithmic features. The idea is to analyse the logic program with respect to a set of properties such as modes, types and termination in order to ensure that the operational behaviour of the program complies with its logic meaning. In this paper, we present an analyser which allows one to integrate many individual analyses previously proposed in the literature as well as new ones. Conceptually, the analyser is based on the notion of abstract sequence which makes it possible to collect all kinds of desirable information including for instance determinacy and multiplicity of a procedure. Keywords: Program Verification, Static Analysis, Logic Programming, Prolog. 1 Introduction The implementation of declarative languages often includes "impure" featur...