Modelling Constraint Logic Programs (for analysis)

Question

Object-Oriented programs can be modelled by different models such as Automata, Process Algebras, Petri Nets or UML. Some of these models can be used to perform various kind of analysis to spot problem in performance or design.

I am studying about logic programming and wondered if there is such kind of models for CLP? How do you do analysis of CLP programs?

Answer 1

The two approaches that I have seen used the most are abstract interpretation and evolving algbras (aka Abstract State Machines). Egon Boerger published a formal definition of Prolog and a correctnes proof of the Warren Abstract Machine using evolving algebras. Pure logic programming languages can just be modelled directly in logic.

Answer 2

Be sure not to miss cTI_lt (constraint based termination inference for left termination)!

Termination inference is an annotation free generalization of termination analysis/checking. It shifts the programmer's focus away from particular cases to the whole relation. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided by the user, which is rather cumbersome if the programs have been written previously without any annotations. With termination inference no annotations are necessary. All provably terminating classes to all related predicates are inferred at once, illustrating the 'multi-directionality' of predicates. This means that predicates can be used safely in several 'directions'.