|
|
|---|
|
|
|
|---|
Program equivalence.
We introduce a notion of equivalence of ACL2 programs here: in terms of the ``top-level'' semantic function exec-call: two programs are equivalent exactly when all function calls yield identical outcomes with respect to the two programs.
This is a functional equivalence: the two programs may have different non-functional properties, i.e. the same function call may take a different number of steps in the two programs (presumably because it is defined differently, or some other function directly or indirectly called by it is defined differently); but the two outcomes will be the same.
The equality of the two outcomes may involve errors or non-termination, besides termination without errors. That is, one yields an error iff the other one does; and one does not terminate iff the other one does not.
It is possible to define both stronger and weaker notions of program equivalence. A stronger notion could take non-functional properties into account. A weaker notion could only take certain function calls into account. We may revise our definition of program equivalence in the future, or perhaps introduce multiple such notions, which may be useful for different purposes.