5
$\begingroup$

I understand that the general problem of program equivalence is undecidable, but I'm wondering what approaches exist to tackle the problem? I am familiar with Hoare-style verification, but are there any other frameworks for proving program equivalence?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ This is a pretty general question: in general program verification is domain specific: you're trying to verify something in particular, e.g. safety or security, or the programs themselves are in a very constrained language. Do you have use-cases in mind? Are you trying to verify full functional equivalence? Something even stronger? $\endgroup$
    – cody
    May 13, 2020 at 13:15

2 Answers 2

Reset to default
1
$\begingroup$

One general approach to the problem is to prove program equivalence by showing the programs have the same semantics. Hoare-style verification, as you say, is one option categorized as axiomatic semantics. Have a look at this article which describes most of the semantic approaches out there, including denotational semantics and operational semantics.

Improve this answer
$\endgroup$
0
$\begingroup$

Proving this via a detour to a semantics is unnecessary and cumbersome.

Hoare logic is for showing that correctness conditions (AKA Hoare triples) of the form $\{\phi\}P\{\psi\}$ hold. To show equivalence of $P$ and $Q$, you'd have to show that $$\{\phi\}P\{\psi\}$\quad\text{iff}\quad\{\phi\}Q\{\psi\}$$ for all pairs $(\phi,\psi)$ of pre- and postconditions. You could attempt that using a symbolic postcondition and then compare the two weakest preconditions. Dijkstra showed how to do that in the 70ies.

A more modern way of doing the same thing would be to use a refinement calculus to show that the two programs under consideration mutually refine each other. Consult any of the good books on the topic, e.g., Carroll Morgan's Programming from Specifications.

Improve this answer
$\endgroup$
2
  • $\begingroup$ How is proving the equivalence of two programs by comparing their semantics a “detour”? Syntactic methods are rarely sufficient except to prove minor program transformations (such as many transformations done by compilers and optimizers). $\endgroup$
    – Gilles 'SO- stop being evil'
    Feb 3, 2022 at 17:26
  • $\begingroup$ What do you mean by "rarely sufficient". These methods are relatively complete (in the sense of Cook). $\endgroup$
    – Kai
    Feb 3, 2022 at 22:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.