Analysing Logic Programs by Reasoning Backwards

Jacob M. Howe, Andy King, and Lunjin Lu

In Maurice Bruynooghe and Kung-Kiu Lau, editors, Program Development in Computational Logic, volume 3049 of Lecture Notes in Computer Science, pages 152-188. Springer-Verlag, May 2004 Also see http://www.springer.de/comp/lncs/index.html.

Abstract

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.

Download publication 481 kbytes (PostScript)

Bibtex Record

@inproceedings{1778,
author = {Jacob M.~Howe and Andy King and Lunjin Lu},
title = {Analysing {L}ogic {P}rograms by {R}easoning {B}ackwards},
month = {May},
year = {2004},
pages = {152-188},
keywords = {},
note = {Also see http://www.springer.de/comp/lncs/index.html.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2004/1778},
    publication_type = {inproceedings},
    submission_id = {6026_1074866841},
    booktitle = {Program Development in Computational Logic},
    editor = {Maurice Bruynooghe and Kung-Kiu Lau},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
    volume = {3049},
}