School of Computing

Verifying termination and error-freedom of logic programs with block declarations

Jan-Georg Smaus, Patricia Hill, and Andy King

Theory and Practise of Logic Programming, pages 182-196, January 2001.

Abstract

Verifying Termination and Error-Freedom of Logic Programs with block Declarations

JAN-GEORG SMAUS PATRICIA HILL ANDY KING

We present verification methods for logic programs with delay declarations. The verified properties are termination and freedom from errors related to built-ins. Concerning termination, we present two approaches. The first approach tries to eliminate the well-known problem of speculative output bindings. The second approach is based on identifying the predicates for which the textual position of an atom using this predicate is irrelevant with respect to termination. Three features are distinctive of this work: it allows for predicates to be used in several modes; it shows that block declarations, which are a very simple delay construct, are sufficient to ensure the desired properties; it takes the selection rule into account, assuming it to be as in most Prolog implementations. The methods can be used to verify existing programs and assist in writing new programs.

Download publication 454 kbytes (PostScript)

Bibtex Record

@article{1068,
author = {Jan-Georg Smaus and Patricia Hill and Andy King},
title = {Verifying Termination and Error-Freedom of Logic Programs with block Declarations},
month = {January},
year = {2001},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2001/1068},
    journal = {Theory and Practise of Logic Programming},
    publication_type = {article},
    publisher = {Cambridge University Press},
    submission_id = {28390_962374127},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014