2

Formal analysis today is usually done on module or unit level. Unfortunately I'm not aware of a common metric which allows to predict if a formal analysis will be possible. Only structurally very simple codes can be formally analysed even with LOC's or cyclomatic complexities of up to a million. In your case here the code of any of the two programs is ...


1

One could write an entire book surveying techniques of proving program equivalence. This answer is just as a very short starting point: Theoretically, if you think about your programs as Turing Machines, then all hope is lost -- proving that two TMs have the same language (i.e., they are semantically equivalent) is undecidable (in fact, it's not in RE$\cup$ ...


Only top voted, non community-wiki answers of a minimum length are eligible