Skip to Main content Skip to Navigation
Conference papers

A Language-Independent Proof System for Mutual Program Equivalence

Abstract : Two programs are mutually equivalent if they both diverge or they end up in similar states. Mutual 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 mutual equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: if it terminates then it establishes the mutual 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/hal-01030754
Contributor : Mister Dart <>
Submitted on : Tuesday, July 22, 2014 - 1:37:44 PM
Last modification on : Thursday, August 1, 2019 - 2:12:06 PM
Long-term archiving on: : Tuesday, November 25, 2014 - 11:05:14 AM

File

submission.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01030754, version 1

Collections

Citation

Ştefan Ciobâcǎ, Dorel Lucanu, Vlad Rusu, Grigore Rosu. A Language-Independent Proof System for Mutual Program Equivalence. ICFEM'14 - 16th International Conference on Formal Engineering Methods, Nov 2014, Luxembourg-Ville, Luxembourg. ⟨hal-01030754⟩

Share

Metrics

Record views

384

Files downloads

404