
FiniteTree Analysis for Constraint LogicBased Languages (TR)[Page last updated on "January 13, 2005, 15:31:42".]Roberto Bagnara, Roberta Gori, Patricia M. Hill, and Enea Zaffanella AbstractLogic languages based on the theory of rational, possibly infinite, trees have much appeal in that rational trees allow for faster unification (due to the omission of the occurscheck) and increased expressivity. Note that cyclic terms can provide a very efficient representation of grammars and other useful objects. Unfortunately, the use of infinite rational trees has problems. For instance, many of the builtin and library predicates are illdefined for such trees and need to be supplemented by runtime checks whose cost may be significant. Moreover, some widelyused program analysis and manipulation techniques are only correct for those parts of programs working over finite trees. It is thus important to obtain, automatically, a knowledge of those program variables (the finite variables) that, at the program points of interest, will always be bound to finite terms. For these reasons, we propose here a new dataflow analysis that captures such information. We present a parametric domain where a simple component for recording finite variables is coupled with a generic domain (the parameter of the construction) providing sharing information. The sharing domain is abstractly specified so as to guarantee the correctness of the combined domain and the generality of the approach.
Available: PDF, 300 DPI, 600 DPI, and 1200 DPI PostScript, DVI, and BibTeX entry. 

enea.zaffanella@unipr.it 
 Home  Personal Info  Research  Papers  Teaching  About 