A COMPOSITIONAL SEMANTIC BASIS FOR THE ANALYSIS OF EQUATIONAL HORN PROGRAMS

We introduce a compositional characterization of the operational seman tics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincid e. We define an abstract narrower mimicking this semantics, and show h ow it can be used as a basis for efficient AND-compositional program a nalysis. As an application of our framework, we show a compositional a nalysis to detect the unsatisfiability of an equation set with respect to a given equational theory. We also show that our method allows us to perform computations and analysis incrementally in a Constraint Equ ational setting and that the test of satisfiability in this setting ca n be done in parallel.