Skip to main content

Inferring non-suspension conditions for logic programs with dynamic scheduling

Genaim, Samir, King, Andy (2008) Inferring non-suspension conditions for logic programs with dynamic scheduling. ACM Transactions on Computational Logic, 9 (3). pp. 182-196. ISSN 1529-3785. (doi:10.1145/1352582.1352585) (KAR id:15105)

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 subgoal selection. The order of subgoal selection is often controlled with delay declarations that specify that a subgoal 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 subgoal that suspends indefinitely. Suspending subgoals 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 article 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 article 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 realized as two simple fixpoint computations. In terms of computation, by modeling n! different schedulings of n subgoals with a single Boolean function, it is possible to reason about the suspension behavior of large programs. In particular, the analysis is fast enough to be applied repeatedly within the program development cycle. The article also demonstrates that the method is precise enough to locate bugs in existing programs.

Item Type: Article
DOI/Identification number: 10.1145/1352582.1352585
Uncontrolled keywords: languages; theory; verification; abstract interpretation; concurrency; logic programming; debugging
Subjects: A General Works
Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Suzanne Duffy
Date Deposited: 04 Mar 2009 14:23 UTC
Last Modified: 16 Nov 2021 09:53 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/15105 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.