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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
https://hdl.handle.net/11365/38349
Attenzione
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo