Non-Failure Analysis for Logic Programs
Saumya Debray Pedro
López-García Manuel
Hermenegildo
Abstract
We provide a method whereby, given mode and (upper approximation)
type information, we can detect procedures and goals that can be
guaranteed to not fail
(i.e., to produce at least one solution or not terminate).
The technique is based on an intuitively very simple notion, that of
a (set of) tests ``covering'' the type of a set of variables. We
show that the problem of determining a covering is undecidable in
general, and give decidability and complexity results for the
Herbrand and linear arithmetic constraint systems. We give sound
algorithms for determining covering that are precise and efficient
in practice. Based on this information, we show how to identify
goals and procedures that can be guaranteed to not fail at runtime.
Applications of such non-failure information include programming
error detection, program transformations
and avoiding speculative parallelism and estimating lower bounds on the
computational costs of goals, which can be used for granularity
control.
Finally, we report on an implementation of our method and show that
better results are obtained than with previously proposed approaches.