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
A type-based framework for locating errors in constraint logic programs
Linköping University, Department of Computer and Information Science. Linköping University, The Institute of Technology.
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: urn:nbn:se:liu:diva-35577Local ID: 27725ISBN: 91-7373-422-5 (print)OAI: oai:DiVA.org:liu-35577DiVA: diva2:256425
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
List of papers
1. Inferring call and success types for CLP programs
Open this publication in new window or tab >>Inferring call and success types for CLP programs
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.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-87992 (URN)
Note

EPSRIT DiSCiPl deliverable, September 1998

Available from: 2013-01-28 Created: 2013-01-28 Last updated: 2013-01-31Bibliographically approved
2. Locating type errors in untyped CLP programs
Open this publication in new window or tab >>Locating type errors in untyped CLP programs
2000 (English)In: Analysis and Visualization Tools for Constraint Programming: Constraint Debugging / [ed] Pierre Deransart, Manuel V. Hermenegildo, Jan Małuszynski, Springer Berlin/Heidelberg, 2000, Vol. 1870, 121-150 p.Chapter in book (Refereed)
Abstract [en]

This book is the first one entirely devoted to the topic of constraint debugging; it presents new approaches to debugging for the computational paradigm of constraint programming. The book is based on the European research project DiSCiPl. It consists of an introduction and three parts, each of them composed of several chapters. The introduction presents the DiSCiPl debugging methodology and explains how the technical chapters are related. The three parts on correctness debugging, performance debugging, and user cases offer a total of 13 consistenly written chapters

Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2000
Series
Lecture Notes in Computer Science, ISSN 0302-9743 (print), 1611-3349 (online) ; 1870
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-48164 (URN)10.1007/10722311_5 (DOI)978-3-540-41137-6 (ISBN)978-3-540-40016-5 (ISBN)3-540-41137-2 (ISBN)
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2014-01-09Bibliographically approved
3. Using parametric set constraints for locating errors in CLP programs
Open this publication in new window or tab >>Using parametric set constraints for locating errors in CLP programs
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.

Keyword
Constraint logic programming, Debugging, Descriptive types, Parametric types, Program correctness, Set constraints, Term grammars
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-46959 (URN)10.1017/S1471068402001473 (DOI)
Available from: 2009-10-11 Created: 2009-10-11 Last updated: 2013-01-28
4. Improving goal directed bottom-up evaluation of logic programs
Open this publication in new window or tab >>Improving goal directed bottom-up evaluation of logic programs
(English)Manuscript (preprint) (Other academic)
Abstract [en]

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.

Keyword
magic-sets, bottom-up evaluation
National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-87997 (URN)
Available from: 2013-01-28 Created: 2013-01-28 Last updated: 2013-01-28
5. The TELL diagnosis tool
Open this publication in new window or tab >>The TELL diagnosis tool
(English)Manuscript (preprint) (Other academic)
Abstract [en]

No abstract available.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:liu:diva-87999 (URN)
Available from: 2013-01-28 Created: 2013-01-28 Last updated: 2013-01-28

Open Access in DiVA

No full text

Authority records BETA

Pietrzak, Pawel

Search in DiVA

By author/editor
Pietrzak, Pawel
By organisation
Department of Computer and Information ScienceThe Institute of Technology
Computer Science

Search outside of DiVA

GoogleGoogle Scholar

isbn
urn-nbn

Altmetric score

isbn
urn-nbn
Total: 61 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