Program Equivalence (was Interesting summary of compiler optimzation testing)

>From: hammond@latour.bellcore.com (Rich A. Hammond)
>Subject: Testing optimizing compilers
>I'd love to have a program that could compare two assembly language
>programs and decide that they functioned identically, but I view that
>as harder than writing the optimizer to begin with.


It's not harder, it's easier. Namely because it's impossible.
Program equivalence is, in general, an unsolvable problem.
Consider:
Program A outputs a 3 and halts.
Program B loops forever.


Clearly Programs A and B don't function identically, but, in general,
a program cannot be written to tell us that. In particular, we cannot
tell that Program B loops forever (this is the Halting Problem).
[It's certainly true that the halting problem is in general undecidable,
but that doesn't preclude the possibility that an interesting subset of
the problem can be solved. In the case above, for example, static analysis
might find that program B has no statement that could output a 3, and so
prove that that particular pair of programs aren't the same. The general
field of proving programs correct seems to me to consist of proving that a
program is equivalent to a specification that is considered correct by
definition. Perhaps there's some interesting stuff there. -John]
--
ARPA: costanzo@cs.rochester.edu
UUCP: ..!{allegra,decvax,seismo}!rochester!costanzo
USnail: CS Dept., University of Rochester, Rochester NY 14627
Phone: (716)275-7747 Spoken: Hey You!


--

Return to the comp.compilers page.
Search the comp.compilers archives again.