This paper proposes a tool to support reasoning about (partial) correctness of constraint logic programs. The tool infers a specification that approximates the semantics of a given program. The main intended application is program debugging. We deal with a "callsuccess "semantics of CLP. We consider a restricted class of specifications, which are regular types of constrained atoms. The call-success semantics of a CLP program is characterized by the declarative semantics of another CLP program ("magic transformation"). Then bottom-up abstract interpretation is used to approximate the latter. We study the theoretical background of this approach.

We are mainly interested in applying it to CLP over finite domains. Our prototype program analyzer works for the programming language CHIP. 1 Introduction and motivation The work reported addresses the problem of correctness of CLP programs. Intuitively, a program is correct if it behaves as expected by the user. But user expectations are seldo.

This chapter presents a static diagnosis tool that locates type errors in untyped CLP programs without executing them. The exciting prototype is specialised for the programming language CHIP [4.10], but the idea applies to any CLP language. The tool works with approximated specifications which describe types of procedure calls and successes. The specifications ar expressed as a certain kind of term grammars. The tool automatically locates at compile time all the errors (with respect to a given specification) in a program. The located erroneous program fragments ar (prefixes of ) clauses. The tool aids the user in constructing specifications incrementally; often a fragment of the specification is already sufficient to locate an error. The presentation is informal. The focus is on the motivation of this work and on the functionality of the tool. Some related formal aspects ar discussed in [4.15, 4.29].

This paper introduces a framework of parametric descriptive directional types for Constraint Logic Programming (CLP). It proposes a method for locating type errors in CLP programs, and presents a prototype debugging tool. The main technique used is checking correctness of programs w.r.t. type specifications. The approach is based on a generalization of known methods for proving the correctness of logic programs to the case of parametric specifications. Set constraint techniques are used for formulating and checking verification conditions for (parametric) polymorphic type specifications. The specifications are expressed in a parametric extension of the formalism of term grammars. The soundness of the method is proved, and the prototype debugging tool supporting the proposed approach is illustrated on examples. The paper is a substantial extension of the previous work by the same authors concerning monomorphic directional types.

This paper introduces a new strategy for goal directed bottom-up evaluation of logic programs. The strategy is based on a combination of two known techniques: dividing a program into strongly connected components (SCC) and Induced Magic-sets.

In our approach no magic transformation is needed (as in Induced Magic-sets). We introduce a notion of a call-success dependency graph that constructed directly from the original program. Its SCCs are used to optimize a fixpoint computation (i.e. they coincide with SCCs of a corresponding magic program). The new graph contains substantially fewer edges than standard dependency graph of a magic program, and thus its SCCs are computed faster. We also show how to incorporate SCC-based optimization into the Unduced Magic-sets technique. This is achived by modifying the basic Induced Magic method, so that the fixpoints are computed locally for every SCC.

The impact of our method is illustrated by experimental results.

No abstract available.