School of Computing

Domain construction for mode analysis of typed logic programs

Jan-Georg Smaus, Pat Hill, and Andy King

Technical Report 8-97, March 1997.

Abstract

Domain Construction for Mode Analysis of Typed Logic Programs

Jan-Georg Smaus, Patricia M. Hill, Andy M. King

TR no. 8-97

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 non-variable 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 Godel.

Download publication 78 kbytes

Bibtex Record

@techreport{151,
author = {Jan-Georg Smaus and Pat Hill and Andy King},
title = {Domain Construction for Mode Analysis of Typed Logic Programs},
month = {March},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/151},
    number = {8-97},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014