Trace slicing is a widely used technique for execution trace analysis that is effectively used in program debugging, analysis and com- prehension. In this paper, we present a backward trace slicing technique that can be used for the analysis of Rewriting Logic theories. Our trace slicing technique allows us to systematically trace back rewrite sequences modulo equational axioms (such as associativity and commu- tativity) by means of an algorithm that dynamically simplifies the traces by detecting control and data dependencies, and dropping useless data that do not influence the final result. Our methodology is particularly suitable for analyzing complex, textually-large system computations such as those delivered as counter-example traces by Maude model-checkers.
We have presented a backward trace-slicing technique for rewriting logic theories. The key idea consists in tracing back ---through the rewrite sequence--- all the relevant symbols of the final state that we are interested in. Preliminary experiments demonstrate that the system works very satisfactorily on our benchmarks ---e.g., we obtained trace slices that achieved a reduction of up to almost @math a @math b @math ab @math ab c d @math x @math (x) @math @math @math (x) @math ( ,P) @math = s t @math P @math t @math s$. The tracing proceeds forward, while ours employs a backward strategy that is particularly convenient for error diagnosis and program debugging. Finally, @cite_13 and @cite_20 apply to TRSs whereas we deal with the richer framework of RWL that considers equations and equational axioms, namely rewriting modulo equational theories.
@cite_13 @cite_20
1494096444 598205067
Program slicing is a useful technique for debugging, testing, and analyzing programs. A program slice consists of the parts of a program which (potentially) affect the values computed at some point of interest. With rare exceptions, program slices have hitherto been computed and defined in ad-hoc and language-specific ways. The principal contribution of this paper is to show that general and semantically well-founded notions of slicing and dependence can be derived in a simple, uniform way from term rewriting systems (TRSs). Our slicing technique is applicable to any language whose semantics is specified in TRS form. Moreover, we show that our method admits an efficient implementation. 1. Abstract reduction systems 2. First-order term rewriting systems 3. Examples of TRSs and special rewriting formats 4. Orthogonality 5. Properties of rewriting: decidability and modularity 6. Termination 7. Completion of equational specifications 8. Equivalence of reductions 9. Strategies 10. Lambda calculus 11. Higher order rewriting 12. Infinitary rewriting 13. Term graph rewriting 14. Advanced ARS theory 15. Rewriting based languages and systems 16. Mathematical background.