TRSynth: a tool for automatic inference of term equivalence in left-linear term rewriting systems.

ABSTRACTThis paper presents a "proof of concept" prototype which is an instance of a semantics-based technique to automatically infer algebraic property-oriented specifications from Term Rewriting Systems. Namely, given the source code of a TRS we infer a specification which consists of a set of equations relating (nested) terms (operation calls) that rewrite, for all possible instantiations, to the same set of values. In the the TRS formalism there are several additional issues which arise with respect to the (first order) functional programming case, because variables are admitted in queries and nonconstructor-based rules are allowed. The glass-box semantic-based inference method that we propose can cope with these issues.