johnl@ima.UUCP (06/15/87)
>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! -- Send compilers articles to ima!compilers or, in a pinch, to Levine@YALE.ARPA Plausible paths are { ihnp4 | decvax | cbosgd | harvard | yale | cca}!ima Please send responses to the originator of the message -- I cannot forward mail accidentally sent back to compilers. Meta-mail to ima!compilers-request