We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis 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 Equational setting and that the test of satisfiability in this setting can be done in parallel.

Alpuente, M., Falaschi, M., Vidal, G. (1996). Compositional Analysis for Equational Horn Programs. In Proc. Algebraic and Logic Programming, 4th International Conference, ALP'94 (pp.133-169). Amsterdam : Elsevier [10.1016/0304-3975(96)00043-6].

Compositional Analysis for Equational Horn Programs

FALASCHI, MORENO;
1996-01-01

Abstract

We introduce a compositional characterization of the operational semantics of equational Horn programs. Then we show that this semantics and the standard operational semantics based on (basic) narrowing coincide. We define an abstract narrower mimicking this semantics, and show how it can be used as a basis for efficient AND-compositional program analysis. As an application of our framework, we show a compositional analysis 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 Equational setting and that the test of satisfiability in this setting can be done in parallel.
1996
3540584315
Alpuente, M., Falaschi, M., Vidal, G. (1996). Compositional Analysis for Equational Horn Programs. In Proc. Algebraic and Logic Programming, 4th International Conference, ALP'94 (pp.133-169). Amsterdam : Elsevier [10.1016/0304-3975(96)00043-6].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11365/38349
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo