Smaus, J.G. and Hill, P.M. and King, A.
(1998)
Verification of Logic Programs with block Declarations Running in Several Modes.
Technical report.
University of Kent, Canterbury, CT2 7NF, United Kingdom
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.
- Depositors only (login required):
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_postscript.png)
