ON THE DESIGN OF A CORRECT FREENESS ANALYSIS FOR LOGIC PROGRAMS

Citation
M. Codish et al., ON THE DESIGN OF A CORRECT FREENESS ANALYSIS FOR LOGIC PROGRAMS, The journal of logic programming, 28(3), 1996, pp. 181-206
Citations number
21
Categorie Soggetti
Computer Sciences, Special Topics","Computer Science Theory & Methods
ISSN journal
07431066
Volume
28
Issue
3
Year of publication
1996
Pages
181 - 206
Database
ISI
SICI code
0743-1066(1996)28:3<181:OTDOAC>2.0.ZU;2-Y
Abstract
Several proposals for computing freeness information for logic program s have been put forward in the recent literature. The availability of such information has proven useful in a variety of applications, inclu ding parallelization of Prolog programs, optimizations in Prolog compi lers, as well as for improving the precision of other analyses. While these proposals have illustrated the importance of such analyses, they lack formal justification. Moreover, several have been found incorrec t. This paper introduces a novel domain of abstract equation, systems describing possible sharing and definite freeness of terms in a system of equations. A simple and intuitive abstract unification algorithm i s presented, providing the core of a correct and precise sharing and f reeness analysis for logic programs. Our contribution is not only a co rrect algorithm, but perhaps primarily, the application of a systemati c approach in which it is derived by mimicking each step in a suitable concrete unification algorithm. Consequently, the abstract algorithm is intuitive-as it resembles the concrete algorithm. It is amenable to formal justification-as the proof of correctness is reduced to showin g that each step in the concrete algorithm is mimicked by a correspond ing step in the abstract algorithm. Finally, it is precis as each step mimics only those situations which can arise in the concrete algorith m.