Skip to main content

Analysing Logic Programs by Reasoning Backwards: A Decade of Research Advances in Logic-Based Program Development

Howe, Jacob M. and King, Andy and Lu, Lunjin (2004) Analysing Logic Programs by Reasoning Backwards: A Decade of Research Advances in Logic-Based Program Development. In: Bruynooghe, Maurice and Lau, Kung-Kiu, eds. Program Development in Computational Logic. Lecture Notes in Computer Science, 3049 . Springer, pp. 152-188. ISBN 978-3-540-22152-4. (doi:10.1007/978-3-540-25951-0_6) (KAR id:37608)

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


One recent advance in program development has been the application of abstract interpretation to verify the partial correctness of a (constraint) logic program. Traditionally forwards analysis has been applied that starts with an initial goal and traces the execution in the direction of the control-flow to approximate the program state at each program point. This is often enough to verify assertions that a property holds. The dual approach is to apply backwards analysis to propagate properties of the allowable states against the control-flow to infer queries for which the program will not violate any assertion. Backwards analysis also underpins other program development tasks such as verifying the termination of a logic program or proving that a logic program with a delay mechanism cannot reduce to a state that contains sub-goals which suspend indefinitely. This paper reviews various backwards analyses that have been proposed for logic programs, identifying common threads in these techniques. The analyses are explained through a series of worked examples. The paper concludes with some suggestions for research in backwards analysis for logic program development.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-540-25951-0_6
Subjects: A General Works
A General Works > AC Collections. Series. Collected works
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 13 Dec 2013 08:34 UTC
Last Modified: 16 Nov 2021 10:14 UTC
Resource URI: (The current URI for this page, for reference purposes)
King, Andy:
  • Depositors only (login required):


Downloads per month over past year