© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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 182-196. 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 = {182-196}, keywords = {determinacy analysis, Craig interpolants}, 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}, }