Domain Construction for Mode Analysis of Typed Logic Programs

There are many applications where precise mode analysis is required. However, within the framework of abstract interpretation, the precision of an analyser depends, in part, on the expressiveness of the abstract domain and its associated abstraction function. This paper considers abstract domains for polymorphically typed logic programs where each nonvariable symbol is explicitly typed. We show how to construct precise domains and their abstraction functions that reflect the declared structure of terms. This domain construction is modular in that an abstract domain for a type does not depend on modules that import this type. A program is abstracted by replacing the unification operations with abstract unification operations. The precision of the domains is demonstrated for several examples using Godel programs. Correctness of the method is proven. The domain construction has been implemented in Gödel