School of Computing

Preventing instantiation errors and loops for logic programs with several modes using t block declarations

Jan-Georg Smaus, Pat Hill, and Andy King

Technical Report UMCS-98-6-1 (University of Manchester), June 1998 Extended abstract. Accepted for presentation at the LOPSTR 98 workshop.

Abstract

We present verification methods for logic programs with delay declarations, showing how type and instantiation errors related to built-ins can be avoided, and how termination can be ensured. Three features are distinctive of this work: (a) we assume that predicates can be used in several modes; (b) we show that block declarations, which are a particularly simple delay construct, are sufficient to ensure the desired properties; (c) we take the selection rule into account, assuming it to be the rule of most Prolog implementations. These methods can be used both to verify existing programs and to assist in writing new programs.

Download publication 182 kbytes (PostScript)

Bibtex Record

@misc{585,
author = {Jan-Georg Smaus and Pat Hill and Andy King},
title = {Preventing Instantiation Errors and Loops for Logic Programs with Several Modes Using {	t block} Declarations},
month = {June},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Extended abstract. Accepted for presentation at the LOPSTR 98 workshop.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/585},
    howpublished = {Technical Report UMCS-98-6-1 (University of Manchester)},
}

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

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

Last Updated: 21/03/2014