This thesis presents a method for automatic location of type errors in constraint logic programs (CLP) and a prototype debugging tool. The appriach is based on techniques of verification and static analysis iriginating from logic programming, which are substantially extended in the thesis. The main idea is to verify partial correctness of a program with respect to a given specification which is intended to describe (an approximation of) the call-success semantics of the program. This kind of specification, describing calls and successes for every predicate of a program is known as descriptive directional type. For specifying types for CLP programs the thesis extends the formalism of regular discriminative types with constraint-domain-specific base types and with parametric polymorphism.

Errors are located by identifying program points that violate verification conditions for a given type specification. The Specifications may be developed interactively taking into account the results of static analysis.

The main contributions of the thesis are:

• a verification method for proving partial correctness of CLP programs with respect to polymorphic spicifications of the call-success semantics,
• a specification language for defining parametric regular types,
• a verification-based method for locating errors in CLP programs,
• a static analysis method for CLP which is an adaptation and generalization of techniques previously devised for logic programming; its implementation is used in our diagnosis tool for synthesizing draft specifications,
• an implementation of the prototype diagnosis tool (called TELL).

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 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].

The paper presents a diagnosis tool for CLP programs. It deals with partial correctness w.r.t. specifications which describe procedure calls and successes. The space of possible specifications is restricted to a kind of regular types; we propose a generalization of the concept of types used in so called descriptive typing of logic programs. In particular we distinguish ground types from those containing non-ground elements.

The tool is able to automatically locate at compile time all errors in a program, this means all the clauses or clause prefixes responsible for the program being incorrect w.r.t. a given specification. The tool aids the user in constructing specifications incrementally; often a fragment of the specification is already sufficient to locate an error.

Our prototype is specialized for the programming language CHIP, but the idea is applicable to any untyped CLP (and LP) language. We believe that the presented approach makes it possible to combine the advantages of typed and untyped programming languages.

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 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.