A Program Transformation for Backwards Analysis of Logic Programs

    Research output: Chapter in Book/Report/Conference proceedingBook chapterResearch

    Abstract

    The input to backwards analysis is a program together with properties that are required to hold at given program points. The purpose of the analysis is to derive initial goals or pre-conditions that guarantee that, when the program is executed, the given properties hold. The solution for logic programs presented here is based on a transformation of the input program, which makes explicit the dependencies of the given program points on the initial goals. The transformation is derived from the resultants semantics of logic programs. The transformed program is then analysed using a standard abstract interpretation. The required pre-conditions on initial goals can be deduced from the analysis results without a further fixpoint computation. For the modes backwards analysis problem, this approach gives the same results as previous work, but requires only a standard abstract interpretation framework and no special properties of the abstract domain.
    Original languageEnglish
    Title of host publicationLogic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003
    EditorsMaurice Bruynooghe
    Number of pages14
    Place of PublicationUppsala
    PublisherSpringer
    Publication date2003
    Pages92-105
    ISBN (Print)3-540-22174-3
    Publication statusPublished - 2003
    SeriesLecture Notes in Computer Science
    Volume3018
    ISSN0302-9743

    Cite this

    Gallagher, J. P. (2003). A Program Transformation for Backwards Analysis of Logic Programs. In M. Bruynooghe (Ed.), Logic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003 (pp. 92-105). Uppsala: Springer. Lecture Notes in Computer Science, Vol.. 3018