liu.seSearch for publications in DiVA
Change search
ReferencesLink to record
Permanent link

Direct link
Inferring call and success types for CLP programs
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
1998 (English)Other (Refereed)
Abstract [en]

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.

Place, publisher, year, edition, pages
National Category
Engineering and Technology
URN: urn:nbn:se:liu:diva-87992OAI: diva2:600985

EPSRIT DiSCiPl deliverable, September 1998

Available from: 2013-01-28 Created: 2013-01-28 Last updated: 2013-01-31Bibliographically approved
In thesis
1. A type-based framework for locating errors in constraint logic programs
Open this publication in new window or tab >>A type-based framework for locating errors in constraint logic programs
2002 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

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

Place, publisher, year, edition, pages
Linköping: Linköpings universitet, 2002. 22 p.
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 772
National Category
Computer Science
urn:nbn:se:liu:diva-35577 (URN)27725 (Local ID)91-7373-422-5 (ISBN)27725 (Archive number)27725 (OAI)
Public defence
2002-09-13, Estraden seminarierum, Hus E, Linköpings universitet, Linköping, 13:15 (Swedish)
Available from: 2009-10-10 Created: 2009-10-10 Last updated: 2013-01-28

Open Access in DiVA

No full text

Other links

Link to CiteSeerX

Search in DiVA

By author/editor
Drabent, WlodzimierzPietrzak, Pawel
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 33 hits
ReferencesLink to record
Permanent link

Direct link