School of Computing

Inferring Non-Suspension Conditions for Logic Programs with Dynamic Scheduling

Samir Genaim and Andy King

ACM Transactions on Computational Logic, pages 182-196, November 2008 To appear.

Abstract

A logic program consists of a logic component and a control component. The former is a specification in predicate logic whereas the latter defines the order of sub-goal selection. The order of sub-goal selection is often controlled with delay declarations that specify that a sub-goal is to suspend until some condition on its arguments is satisfied. Reasoning about delay declarations is notoriously difficult for the programmer and it is not unusual for a program and a goal to reduce to a state that contains a sub-goal that suspends indefinitely. Suspending sub-goals are usually unintended and often indicate an error in the logic or the control. A number of abstract interpretation schemes have therefore been proposed for checking that a given program and goal cannot reduce to such a state. This paper considers a reversal of this problem, advocating an analysis that for a given program infers a class of goals that do not lead to suspension. This paper shows that this more general approach can have computational, implementational and user-interface advantages. In terms of user-interface, this approach leads to a lightweight point-and-click mode of operation in which, after directing the analyser at a file, the user merely has to inspect the results inferred by the analysis. In terms of implementation, the analysis can be straightforwardly realised as two simple fixpoint computations. In terms of computation, by modelling n! different schedulings of n sub-goals with a single Boolean function, it is possible to reason about the suspension behaviour of large programs. In particular, the analysis is fast enough to be applied repeatedly within the program development cycle. The paper also demonstrates that the method is precise enough to locate bugs in existing programs.

Download publication 404 kbytes (PDF)

Bibtex Record

@article{2456,
author = {Samir Genaim and Andy King},
title = {Inferring {N}on-{S}uspension {C}onditions for {L}ogic {P}rograms with {D}ynamic {S}cheduling},
month = {November},
year = {2008},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {To appear},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2008/2456},
    publication_type = {article},
    submission_id = {8361_1164103232},
    ISSN = {1529-3785},
    journal = {ACM Transactions on Computational Logic},
    publisher = {Association of Computer Machinery (ACM)},
}

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

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

Last Updated: 21/03/2014