Skip to main content

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

Smaus, Jan-Georg, Hill, Pat, King, Andy (2001) Verifying termination and error-freedom of logic programs with block declarations. Theory and Practice of Logic Programming, 1 (4). pp. 447-486. ISSN 1471-0684. (doi:10.1017/S1471068401001107) (KAR id:37581)

PDF Pre-print
Language: English
Download (1MB) Preview
[thumbnail of content.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL


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.

Item Type: Article
DOI/Identification number: 10.1017/S1471068401001107
Uncontrolled keywords: verification; delay declarations; termination; modes; types; selection rule; built-ins; errors.
Subjects: A General Works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 12 Dec 2013 20:02 UTC
Last Modified: 16 Feb 2021 12:50 UTC
Resource URI: (The current URI for this page, for reference purposes)
King, Andy:
  • Depositors only (login required):


Downloads per month over past year