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

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Using parametric set constraints for locating errors in 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.
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
2002 (English)In: Theory and Practice of Logic Programming, ISSN 1471-0684, E-ISSN 1475-3081, Vol. 2, no 4-5, 549-610 p.Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2002. Vol. 2, no 4-5, 549-610 p.
Keyword [en]
Constraint logic programming, Debugging, Descriptive types, Parametric types, Program correctness, Set constraints, Term grammars
National Category
Engineering and Technology
Identifiers
URN: urn:nbn:se:liu:diva-46959DOI: 10.1017/S1471068402001473OAI: oai:DiVA.org:liu-46959DiVA: diva2:267855
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2017-12-13
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.
Series
Linköping Studies in Science and Technology. Dissertations, ISSN 0345-7524 ; 772
National Category
Computer Science
Identifiers
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

Publisher's full text

Authority records BETA

Drabent, WlodzimierzMaluszynski, JanPietrzak, Pawel

Search in DiVA

By author/editor
Drabent, WlodzimierzMaluszynski, JanPietrzak, Pawel
By organisation
Department of Computer and Information ScienceThe Institute of Technology
In the same journal
Theory and Practice of Logic Programming
Engineering and Technology

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 55 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf