A Language-Independent Proof System for Full Program Equivalence

From FSL
Jump to: navigation, search

J.FOAC

A Language-Independent Proof System for Full Program Equivalence
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
J.FAOC, Volume 28(3), pp 469-497. 2016
Abstract. Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known weather the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).
PDF, Matching Logic, DOI, J.FAOC, BIB

ICFEM'14

A Language-Independent Proof System for Mutual Program Equivalence
Stefan Ciobaca and Dorel Lucanu and Vlad Rusu and Grigore Rosu
ICFEM'14, LNCS 8829, pp 75-90. 2014
Abstract. Two programs are mutually equivalent if they both diverge or they both terminate with the same result. In this paper we introduce a language-independent proof system for mutual equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence.
PDF, Slides(PDF), Matching Logic, DOI, ICFEM'14, BIB


Personal tools
Namespaces

Variants
Actions
Navigation