Program equivalence

History / Edit / PDF / EPUB / BIB
Created: July 6, 2016 / Updated: September 25, 2017 / Status: in progress / 3 min read (~476 words)

Meta inspection
Build the state machine based on the instructions given
Execute a certain amount of test cases to assert equivalence

Consider as different programs
Consider as similar program by going through some reduction steps

If the statement acts on a variable that is not used in the other program, then the two programs can be considered equivalent ...


One cannot use the graph equivalent of a program to directly determine if two program are equivalent
If we can find a program where the largest common graph minor

If two programs admit a common graph minor, then those two programs are structurally similar
If the differing statements can be extracted without altering the behavior of the existing program

  • this is as if two people were thinking about the same thing but one was able to so more computation at the same time or during the same process (for example teaching many more preconditions/postconditions
    • In this case though the resulting behavior is different and one appears more”sophisticated” than the other (one being a subset of the other)