Domain Construction for Mode Analysis of Typed Logic Programs

Smaus, J.G. and Hill, P.M. and King, A. (1997) Domain Construction for Mode Analysis of Typed Logic Programs. Technical report. University of Kent

Postscript
Download (266Kb)
PDF
Download (300Kb)	Preview

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.

Item Type:	Monograph (Technical report)
Uncontrolled keywords:	Logic programming, types, abstract interpretation, mode analysis, polymorphism, abstract domains, Goedel
Subjects:	Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions:	Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User:	Mark Wheadon
Date Deposited:	25 Jul 2009 21:28
Last Modified:	25 Jun 2012 10:15
Resource URI:	http://kar.kent.ac.uk/id/eprint/21531 (The current URI for this page, for reference purposes)

• Depositors only (login required):