Skip to main content
SpringerLink
Log in

Analysing Logic Programs by Reasoning Backwards

  • Chapter
Program Development in Computational Logic

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 3049))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aiken, A., Lakshman, T.K.: Directional Type Checking of Logic Programs. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 43–60. Springer, Heidelberg (1994)

    Google Scholar 

  2. Armstrong, T., Marriott, K., Schachte, P., Søndergaard, H.: Two Classes of Boolean Functions for Dependency Analysis. Science of Computer Programming 31(1), 3–45 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  3. Benoy, F., King, A.: Inferring Argument Size Relationships with CLP(R). In: Gallagher, J.P. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 204–224. Springer, Heidelberg (1997)

    Google Scholar 

  4. Boye, J., Drabent, W., Małuszyński, J.: Declarative Diagnosis of Constraint Programs: an Assertion-based Approach. In: Proceedings of the Third International Workshop on Automated Debugging, pp. 123–141. University of Linköping Press (1997)

    Google Scholar 

  5. Brodsky, A., Sagiv, Y.: Inference of Monotonicity Constraints in Datalog Programs. In: Symposium on Principles of Database Systems, pp. 190–199. ACM Press, New York (1989)

    Google Scholar 

  6. Bruynooghe, M., Leuschel, M., Sagonas, K.: A Polyvariant Binding-Time Analysis for Off-line Partial Deduction. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 27–41. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  7. Carlsson, M.: Freeze, Indexing, and Other Implementation Issues in the WAM. In: Lassez, J.-L. (ed.) International Conference on Logic Programming, pp. 40–58. MIT Press, Cambridge (1987)

    Google Scholar 

  8. Codish, M., Falaschi, M., Marriott, K.: Suspension Analyses for Concurrent Logic Programs. Transactions on Programming Languages and Systems 16(3), 649–686 (1994)

    Article  Google Scholar 

  9. Codish, M., Lagoon, V.: Type Dependencies for Logic Programs using ACIunification. Theoretical Computer Science 238, 131–159 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  10. Codish, M., Taboch, C.: A Semantic Basis for the Termination Analysis of Logic Programs. The Journal of Logic Programming 41(1), 103–123 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  11. Codognet, C., Codognet, P., Corsini, M.: Abstract Interpretation for Concurrent Logic Languages. In: Debray, S.K., Hermenegildo, M.V. (eds.) North American Conference on Logic Programming, pp. 215–232. MIT Press, Cambridge (1990)

    Google Scholar 

  12. Comini, M., Gori, R., Levi, G., Volpe, P.: Abstract Interpretation based Verification of Logic Programs. Electronic Notes of Theoretical Computer Science 30(1) (1999)

    Google Scholar 

  13. Cortesi, B.: Le Charlier, and P. Van Hentenryck. Type Analysis of Prolog using Type Graphs. The Journal of Logic Programming 22(3), 179–208 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  14. Cousot, P., Cousot, R.: Inductive Principles for Proving Invariance Properties of Programs. In: Tools and Notions for Program Construction, pp. 75–119. Cambridge University Press, Cambridge (1982)

    Google Scholar 

  15. Cousot, P., Halbwachs, N.: Automatic Discovery of Linear Restraints Among Variables of a Program. In: Symposium on Principles of Programming Languages, pp. 84–97. ACM Press, New York (1978)

    Google Scholar 

  16. Debray, S.K.: QD-Janus: a Sequential Implementation of Janus in Prolog. Software Practice and Experience 23(12), 1337–1360 (1993)

    Article  Google Scholar 

  17. Debray, S.K., Gudeman, D., Bigot, P.: Detection and Optimization of Suspension-free Logic Programs. The Journal of Logic Programming 29(1-3), 171–194 (1992)

    Article  MathSciNet  Google Scholar 

  18. Dyber, P.: Inverse Image Analysis Generalises Strictness Analysis. Information and Computation 90(2), 194–216 (1991)

    Article  MathSciNet  Google Scholar 

  19. Falaschi, M., Hicks, P., Winsborough, W.: Demand Transformation Analysis for Concurrent Constraint Programs. The Journal of Logic Programming 41(3), 185–215 (2000)

    Article  MathSciNet  Google Scholar 

  20. Gabbrielli, M., Giacobazzi, R.: Goal Independency and Call Patterns in the Analysis of Logic Programs. In: ACM Symposium on Applied Computing, pp. 394–399. ACM Press, New York (1994)

    Google Scholar 

  21. Gabbrielli, M., Levi, G., Meo, M.C.: Resultants Semantics for Prolog. Journal of Logic and Computation 6(4), 491–521 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  22. Gallagher, J.P.: A Program Transformation for Backwards Analysis of Logic Programs. In: Bruynooghe, M. (ed.) Pre-proceedings of the International Symposium on Logic-based Program Synthesis and Transformation. Katholieke Universiteit Leuven, Technical Report, vol. CW 365, pp. 113–122 (2003)

    Google Scholar 

  23. Gallagher, J.P., Puebla, G.: Abstract Interpretation over Non-deterministic Finite Tree Automata for Set-based Analysis of Logic Programs. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 243–261. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  24. Genaim, S., Codish, M.: Inferring Termination Conditions for Logic Programs using Backwards Analysis. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 681–690. Springer, Heidelberg (2001); Technical report version available at http://www.cs.bgu.ac.il/~mcodish/Papers/Pages/lpar01.html

    Chapter  Google Scholar 

  25. Genaim, S., Codish, M., Gallagher, J.P., Lagoon, V.: Combining Norms to Prove Termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 126–138. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  26. Genaim, S., King, A.: Goal-Independent Suspension Analysis for Logic Programs with Dynamic Scheduling. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 84–98. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  27. Giacobazzi, R.: Abductive Analysis of Modular Logic Programs. Journal of Logic and Computation 8(4), 457–484 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  28. Giacobazzi, R., Debray, S.K., Levi, G.: Generalized Semantics and Abstract Interpretation for Constraint Logic Programs. The Journal of Logic Programming 25(3), 191–248 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  29. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making Abstract Domains Condensing. ACM Transactions on Computational Logic (to appear)

    Google Scholar 

  30. Giacobazzi, R., Scozzari, F.: A Logical Model for Relational Abstract Domains. ACM Transactions on Programming Languages and Systems 20(5), 1067–1109 (1998)

    Article  Google Scholar 

  31. Hall, C., Wise, D.: Generating Function Versions with Rational Strictness Patterns. Science of Computer Programming 12, 39–74 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  32. Hanus, M.: Compile-time Analysis of Nonlinear Constraints in CLP(R). New Generation Computing 13(2), 155–186 (1995)

    Article  Google Scholar 

  33. Heaton, A., Abo-Zaed, M., Codish, M., King, A.: A Simple Polynomial Groundness Analysis for Logic Programs. The Journal of Logic Programming 45(1-3), 143–156 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  34. Hoarau, S., Mesnard, F.: Inferring and Compiling Termination for Constraint Logic Programs. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol. 1559, pp. 240–254. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  35. Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C., Roscoe, A.W., Sanders, J.W., Sorensen, I.H., Spivey, J.M., Sufrin, B.: Laws of Programming. Communications of the ACM 30(8), 672–686 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  36. Howe, J.M., King, A.: Abstracting Numeric Constraints with Boolean Functions. Information Processing Letters 75(1-2), 17–23 (2000)

    Article  MathSciNet  Google Scholar 

  37. Howe, J.M., King, A.: Positive Boolean Functions as Multiheaded Clauses. In: Codognet, P. (ed.) ICLP 2001. LNCS, vol. 2237, pp. 120–134. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  38. Howe, J.M., King, A.: Efficient Groundness Analysis in Prolog. Theory and Practice of Logic Programming 3(1), 95–124 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  39. King, A., Lu, L.: A Backward Analysis for Constraint Logic Programs. Theory and Practice of Logic Programming 2, 517–547 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  40. King, A., Lu, L.: Forward versus Backward Verification of Logic Programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 315–330. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  41. King, A., Soper, P.: Schedule Analysis of Concurrent Logic Programs. In: Apt, K.R. (ed.) Joint International Conference and Symposium on Logic Programming, pp. 478–492. MIT Press, Cambridge (1992)

    Google Scholar 

  42. Le Charlier, B., Leclére, C., Rossi, S., Cortesi, A.: Automatic Verification of Prolog Programs. The Journal of Logic Programming 39(1-3), 3–42 (1999)

    Article  MATH  Google Scholar 

  43. Lindenstrauss, N., Sagiv, Y., Serebrenik, A.: Unfolding the Mystery of Mergesort. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS, vol. 1463, pp. 206–225. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  44. Lu, L., King, A.: Backward Type Inference Generalises Type Checking. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 85–101. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  45. Marriott, K., García de la Banda, M., Hermenegildo, M.V.: Analyzing Logic Programs with Dynamic Scheduling. In: Principles of Programming Languages, pp. 240–254. ACM Press, New York (1994)

    Google Scholar 

  46. Marriott, K., Søndergaard, H.: Precise and Efficient Groundness Analysis for Logic Programs. ACM Letters on Programming Languages and Systems 2(4), 181–196 (1993)

    Article  Google Scholar 

  47. Martin, J.C., King, A.: Generating Efficient, Terminating Logic Programs. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 273–284. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  48. Mazur, N., Janssens, G., Bruynooghe, M.: A Module Based Analysis for Memory Reuse in Mercury. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 1255–1269. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  49. Mazur, N., Janssens, G., Van Hoof, V.: Collecting Potential Optimizations. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 109–110. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  50. Mesnard, F.: Inferring Left-terminating Classes of Queries for Constraint Logic Programs. In: Joint International Conference and Symposium on Logic Programming, pp. 7–21. MIT Press, Cambridge (1996)

    Google Scholar 

  51. Mesnard, F., Neumerkel, U.: Applying Static Analysis Techniques for Inferring Termination Conditions of Logic Programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 93–110. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  52. Mesnard, F., Payet, É., Neumerkel, U.: Detecting Optimal Termination Conditions of Logic Programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 509–526. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  53. Mesnard, F., Ruggieri, S.: On Proving Left Termination of Constraint Logic Programs. ACM Transactions on Computational Logic 4(2), 207–259 (2003)

    Article  MathSciNet  Google Scholar 

  54. Naish, L.: Negation and Quantifiers in NU-Prolog. In: Shapiro, E. (ed.) ICLP 1986. LNCS, vol. 225, pp. 624–634. Springer, Heidelberg (1986)

    Google Scholar 

  55. Pedreschi, D., Ruggieri, S.: Weakest Preconditions for Pure Prolog Programs. Information Processing Letters 67(3), 145–150 (1998)

    Article  MathSciNet  Google Scholar 

  56. Puebla, G., Bueno, F., Hermenegildo, M.V.: An Assertion Language for Constraint Logic Programs. In: Deransart, P., Małuszyński, J. (eds.) DiSCiPl 1999. LNCS, vol. 1870, pp. 23–61. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  57. Puebla, G., Bueno, F., Hermenegildo, M.V.: A Generic Preprocessor for Program Validation and Debugging. In: Deransart, P., Małuszyński, J. (eds.) DiSCiPl 1999. LNCS, vol. 1870, pp. 63–107. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  58. Puebla, G., Hermenegildo, M.V.: Abstract Multiple Specialization and its Application to Program Parallelization. The Journal of Logic Programming 41(2&3), 279–316 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  59. Rychlikowski, P., Truderung, T.: Polymorphic Directional Types for Logic Programming. In: International Conference on Principles and Practice of Declarative Programming, pp. 61–72. ACM Press, New York (2001)

    Chapter  Google Scholar 

  60. Saraswat, V.A.: Concurrent Constraint Programming. MIT Press, Cambridge (1993)

    Google Scholar 

  61. Saraswat, V.A., Kahn, K., Levy, J.: Janus: a Step Towards Distributed Constraint Programming. In: North American Conference on Logic Programming, pp. 431–446. MIT Press, Cambridge (1990)

    Google Scholar 

  62. Somogyi, Z., Henderson, F., Conway, T.: The Execution Algorithm of Mercury, an Efficient Purely Declarative Logic Programming Language. The Journal of Logic Programming 29(1-3), 17–64 (1996)

    Article  MATH  Google Scholar 

  63. Vielle, L.: Recursive Query Processing: The Power of Logic. Theoretical Computer Science 69(1), 1–53 (1989)

    Article  MathSciNet  Google Scholar 

  64. Volpe, P.: A First-Order Language for Expressing Aliasing and Type Properties of Logic Programs. Science of Computer Programming 39(1), 125–148 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  65. Wadler, P., Hughes, R.J.M.: Projections for Strictness Analysis. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 385–407. Springer, Heidelberg (1987)

    Google Scholar 

  66. Yardeni, E., Shapiro, E.Y.: A Type System for Logic Programs. The Journal of Logic Programming 10(2), 125–153 (1991)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. City University, London, EC1V 0HB, UK

    Jacob M. Howe

  2. University of Kent, Canterbury, CT2 7NF, UK

    Andy King

  3. Oakland University, Rochester, MI 48309, USA

    Lunjin Lu

Authors
  1. Jacob M. Howe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy King
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lunjin Lu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Katholieke Universiteit Leuven, Belgium

    Maurice Bruynooghe

  2. School of Computer Science, The University of Manchester, M13 9PL, Manchester, United Kingdom

    Kung-Kiu Lau

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Howe, J.M., King, A., Lu, L. (2004). Analysing Logic Programs by Reasoning Backwards. In: Bruynooghe, M., Lau, KK. (eds) Program Development in Computational Logic. Lecture Notes in Computer Science, vol 3049. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-25951-0_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-25951-0_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22152-4

  • Online ISBN: 978-3-540-25951-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation