Speaker:Harald Sondergaard
Time:1999-02-09 ~ 120-NaN-NaN
Place:Rm.3207, Industrial Management Bldg./KAIST

Abstract

1. Boolean functions for dependency analysis

Many static analyses for declarative programming/database languages use Boolean functions to express dependencies among variables or argument positions. Examples include groundness analysis, finiteness analysis and functional dependency analysis for databases. We discuss two classes of Boolean functions that have been used: positive and definite functions, and their efficient implementation for dependency analyses. The talk will also serve as a gentle introduction to groundness analysis using the abstract domain `Pos'.

2. Sharing and groundness dependencies in logic programs

Next to `Pos', the abstract domain which has has attracted most attention in abstract interpretation of logic programs is `Sharing', proposed by Jacobs and Langen for sharing analysis. We re-cast Jacobs and Langen's analysis in terms of the property of "not being affected by the binding of a /single/ variable." The resulting "unaffectedness dependency" analysis reveals a surprisingly close connection with groundness dependency analysis using `Pos'. The new view of sharing analysis improves our understanding of this type of analysis and it leads to an elegant expression of its combination with groundness dependency analysis, that is, of the reduced product of the two analyses. It also opens up new avenues for the efficient implementation of sharing analysis, for example using ROBDDs, as well as efficient implementation of the reduced product, using domain factorisations.

3. A denotational framework for abstract interpretation

Much of the research into abstract interpretation of logic programs has been devoted to designing abstract interpretation "frameworks" which consist of a generic dataflow algorithm with a few base operations as parameters. A given analysis is then obtained by providing these parametric functions. An important property of a framework is that correctness of the resultant analysis is assured as long as the parametric functions correctly approximate the standard interpretation of these parametric functions. Many of these frameworks have been translated into working generic "analysis engines". However, a single framework is not really suitable for all applications. If the operational semantics is changed, say to a "bottom-up" evaluation or to allow dynamic atom scheduling, or if the language is extended, say to allow constraints or negation, then the underlying semantic equations are changed and so a new framework must be designed and proved correct. In this talk we take up F. Nielson's idea that much of the work involved in this can be shifted to the level of some (denotational) meta-language. By a careful choice of the meta-language, properties that are important for proving correctness of dataflow analysis can be established at the level of the meta-language once and for all, rather than establishing them for each framework or analysis.

4. Termination analysis for Mercury

Mercury is a logic/functional programming language designed for large-scale programming. Unlike Prolog, it is strongly typed and moded, and the Mercury compiler capitalises on this to generate programs that are much faster than those produced by any other logic programming system. We describe the termination analyser for Mercury. It deals with full Mercury, including modules and I/O. In spite of these obstacles, it produces excellent termination information, while having a negligible impact on the running time of the compiler of which it is part, even for large programs.

[ List ]