[go: up one dir, main page]
Skip to main content
SpringerLink
Log in

A language-independent proof system for full program equivalence

  • Original Article
  • Published:
Formal Aspects of Computing

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 whether 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).

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Amal Ahmed, Derek Dreyer, Andreas Rossberg (2009) State-dependent representation independence. In POPL 2009, pp 340–353

  2. Tamarah Arons, Elad Elster, Limor Fix, Sela Mador-Haim, Michael Mishaeli, Jonathan Shalev, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi, Lenore D. Zuck (2005) Formal verification of backward compatibility of microcode. In CAV 2005, volume 3576 of LNCS, pp 185–198

  3. Yves Bertot, Pierre Castran (2010) Interactive Theorem Proving and Program Development: Coq’Art The Calculus of Inductive Constructions. Springer, 1st edition

  4. Nick Benton (2004) Simple relational correctness proofs for static analyses and program transformations. In POPL 2004, pp 14–25

  5. Nick Benton, Chung-Kil Hur (2009) Biorthogonality, step-indexing and compiler correctness. In ICFP 2009, pp 97–108

  6. Denis Bogdănaş, Grigore Roşu (2015) K-Java: A Complete Semantics of Java. In POPL 2015, pp 445–456

  7. Ştefan Ciobâcă, Dorel Lucanu, Vlad Rusu, Grigore Roşu (2015) A theoretical foundation for programming language aggregation. In WADT 2014, volume 9463 of LNCS, pp 30–47

  8. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuţă, Brandon M. Moore, Traian Florin Şerbănuţă, Grigore Roşu (2014) All-path reachability logic. In RTA-TLCA’14, volume 8560 of LNCS, pp 425–440

  9. Claudia Elena Chiriţă, Traian Florin Şerbănuţă (2015) An institutional foundation for the \({\mathbb{K}}\) semantic framework. In WADT 2014, volume 9463 of LNCS, pp 9–29

  10. Sagar Chaki, Arie Gurfinkel, Ofer Strichman (2012) Regression verification for multi-threaded programs. In VMCAI 2012, volume 7148 of LNCS, pp 119–135

  11. Ştefan Ciobâcă (2014) Reducing partial equivalence to partial correctness. In SYNASC 2014, pp 164–171. IEEE

  12. Sorin Crăciunescu (2002) Proving the equivalence of CLP programs. In ICLP 2002, volume 2401 of LNCS, pp 287–301

  13. Chucky Ellison, Grigore Roşu (2012) An executable formal semantics of C with applications. In POPL 2012, pp 533–544

  14. Godlin Benny, Strichman Ofer (2008) Inference rules for proving the equivalence of recursive procedures. Acta Informatica 45(6): 403–439

    Article  MathSciNet  MATH  Google Scholar 

  15. Godlin Benny, Strichman Ofer (2013) Regression verification: proving the equivalence of similar programs. Software Testing, Verification and Reliability 23(3): 241–258

    Article  Google Scholar 

  16. Richard K. Guy (1983) Don’t try to solve these problems. The American Mathematical Monthly, 90(1):35–38, 39–41

  17. Chung-Kil Hur, Derek Dreyer (2011) A kripke logical relation between ML and assembly. In POPL 2011, pp 133–146

  18. Chung-Kil Hur, Derek Dreyer, Georg Neis, Viktor Vafeiadis (2012) The marriage of bisimulations and kripke logical relations. In POPL 2012, pp 59–72

  19. Anne Elisabeth Haxthausen, Friederike Nickl (1996) Pushouts of order-sorted algebraic specifications. In AMAST 1996, pp 132–147. Springer-Verlag

  20. Chung-Kil Hur, Georg Neis, Derek Dreyer, Viktor Vafeiadis (2014) A Logical Step Forward in Parametric Bisimulations. Technical Report 003, MPI-SWS, January

  21. Hoare CharlesAntony Richard (1969) An axiomatic basis for computer programming. Communications of the ACM 12(10): 576–580

    Article  MATH  Google Scholar 

  22. Sudipta Kundu, Zachary Tatlock, Sorin Lerner (2009) Proving optimizations correct using parameterized program equivalence. In PLDI 2009, pp 327–337. ACM

  23. Leroy Xavier (2009) Formal verification of a realistic compiler. Communications of the ACM, 52(7): 107–115

    Article  Google Scholar 

  24. Shuvendu K. Lahiri, Chris Hawblitzel, Ming Kawaguchi, Henrique Rebêlo (2012) SYMDIFF: A language-agnostic semantic diff tool for imperative programs. In CAV 2012, volume 7358 of LNCS, pp 712–717

  25. Dorel Lucanu, Vlad Rusu (2014) Program equivalence by circular reasoning. Formal Aspects of Computing, pp 1–26

  26. Dorel Lucanu, Vlad Rusu, Andrei Arusoaie A Generic Framework for Symbolic Execution: Theory and Applications. Journal of Symbolic Computation, to appear

  27. Robin Milner (1989) Communication and concurrency. Prentice Hall

  28. John C. Mitchell (1986) Representation independence and data abstraction. In POPL 1986, pp 263–276

  29. José Meseguer, Grigore Roşu (2004) Rewriting logic semantics: From language specifications to formal analysis tools. In IJCAR 2004, volume 3097 of LNCS, pp 1–44

  30. George Necula (2000) Translation validation for an optimizing compiler. In PLDI 2000, pp 83–94. ACM

  31. Daejun Park, Andrei Ştefănescu, Grigore Roşu (2015) KJS: A complete formal semantics of JavaScript. In PLDI 2015, pp 346–356

  32. Andrew M. Pitts (2002) Operational semantics and program equivalence. In Applied Semantics Summer School, volume 2395 of LNCS, pp 378–412

  33. Grigore Roşu, Andrei Ştefănescu (2012) Checking reachability using matching logic. In OOPSLA, pp 555–574. ACM

  34. Grigore Roşu, Andrei Ştefănescu (2012) Towards a unified theory of operational and axiomatic semantics. In ICALP 2012, volume 7392 of LNCS, pp 351–363

  35. Grigore Roşu, Andrei Ştefănescu, RŞ;tefan Ciobâcă, Brandon M. Moore (2013) One-path reachability logic. In LICS 2013, pp 358–367. IEEE

  36. Grigore Roşu, Chucky Ellison, Wolfram Schulte (2010) Matching logic: An alternative to Hoare/Floyd logic. In AMAST 2010, volume 6486 of LNCS, pp 142–162

  37. John C. Reynolds (2002) Separation logic: A logic for shared mutable data structures. In LICS 2002, pp 55–74

  38. Grigore Roşu (2006) Equality of streams is a \({\Pi}_{2}^{0}\)-complete problem. In ICFP 2006, pp 184–191. ACM

  39. Grigore Roşu (2015) Matching logic—extended abstract. In RTA 2015, volume 36 of LIPIcs, pp 5–21

  40. Davide Sangiorgi (2011) Introduction to Bisimulation and Coinduction. Cambridge University Press, New York, NY, USA

  41. Fabio Somenzi, Andreas Kuehlmann (2006) Electronic Design Automation For Integrated Circuits Handbook, volume 2, chapter 4: Equivalence Checking. CRC Press

  42. Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii (2011) Environmental bisimulations for higher-order languages. ACM Transactions on Programming Languages and Systems, 33(1):5

  43. Traian-Florin Şerbănuţă, Grigore Roşu, José Meseguer (2009) A rewriting logic approach to operational semantics. Information and Computation, 207(2):305–340

Download references

Author information

Authors and Affiliations

  1. Faculty of Computer Science, “Alexandru Ioan Cuza” University, 16, General Berthelot Street, 700483, Iasi, Romania

    Ştefan Ciobâcă & Dorel Lucanu

  2. Inria, Lille, France

    Vlad Rusu

  3. University of Illinois at Urbana-Champaign, Champaign, USA

    Grigore Roşu

Authors
  1. Ştefan Ciobâcă
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dorel Lucanu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vlad Rusu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Grigore Roşu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ştefan Ciobâcă.

Additional information

Stephan Merz, Jun Pang, and Jin Song Dong

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ciobâcă, Ş., Lucanu, D., Rusu, V. et al. A language-independent proof system for full program equivalence. Form Asp Comp 28, 469–497 (2016). https://doi.org/10.1007/s00165-016-0361-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00165-016-0361-7

Keywords

Search

Navigation