School of Computing

Verification of logic programs with block declarations running in several modes

Jan-Georg Smaus, Pat Hill, and Andy King

Technical Report 7-98, University of Kent at Canterbury, Canterbury, CT2 7NF, United Kingdom, July 1998.

Abstract

We present several verification methods for logic programs with delay declarations, dealing with five aspects of verification: occur-check freedom, flounder freedom, preventing errors related to built-ins, unification freedom, and termination. These methods can be used to verify existing programs, and to assist in writing new programs. Three features are distinctive of this work: we assume that predicates can be used in several modes; we show that block declarations, which are a very simple delay construct, are sufficient; we take the selection rule into account, assuming it to be as in most Prolog implementations. Our results on the first two aspects are straightforward generalisations of previous results. The most important contribution of this work is about termination. The method for proving termination is based on identifying the so-called robust predicates, for which the textual position of an atom using this predicate is irrelevant.

Download publication 445 kbytes (PostScript)

Bibtex Record

@techreport{602,
author = {Jan--Georg Smaus and Pat Hill and Andy King},
title = {Verification of Logic Programs with block Declarations  Running in Several Modes},
month = {July},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/602},
    address = {Canterbury, CT2 7NF, United Kingdom},
    institution = {University of Kent at Canterbury},
    number = {7-98},
}

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

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

Last Updated: 21/03/2014