caa a22 4500 605516359 CHVBK 20210128100713.0 cr unu---uuuuu 210128e20150701xx s 000 0 eng 10.1007/s00165-014-0319-6 doi (NATIONALLICENCE)springer-10.1007/s00165-014-0319-6 Program equivalence by circular reasoning [Elektronische Daten] [Dorel Lucanu, Vlad Rusu] We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences and is appropriate for deterministic (or, at least, for confluent) programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves the equivalence of (infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. The approach is illustrated by proving program equivalence in two languages from different programming paradigms. The examples in the paper, as well as other examples, can be checked using an online tool. British Computer Society, 2014 Program equivalence nationallicence Proof system nationallicence Language independence nationallicence Lucanu Dorel Al. I. Cuza University of Iaşi, Iasi, Romania aut Rusu Vlad Inria Lille Nord-Europe, Lille, France aut Formal Aspects of Computing Springer London 27/4(2015-07-01), 701-726 0934-5043 27:4<701 2015 27 165 https://doi.org/10.1007/s00165-014-0319-6 text/html Onlinezugriff via DOI BK010053 XK010053 XK010000 Metadata rights reserved Springer special CC-BY-NC licence nationallicence 1 research-article jats NATIONALLICENCE NATIONALLICENCE NL-springer NATIONALLICENCE 856 40 https://doi.org/10.1007/s00165-014-0319-6 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Lucanu Dorel Al. I. Cuza University of Iaşi, Iasi, Romania aut NATIONALLICENCE 700 1- Rusu Vlad Inria Lille Nord-Europe, Lille, France aut NATIONALLICENCE 773 0- Formal Aspects of Computing Springer London 27/4(2015-07-01), 701-726 0934-5043 27:4<701 2015 27 165