Proof of Greatest Number Program and Find
Zhihui Shan, Qiang Han, Meng Han · 2021 8th International Conference on Dependable Systems and Their Applications (DSA) · 2021
It is very difficult for software testing to enumerate all possible situations. This method can’t guarantee the correctness of the program, so strict mathematical formulas are needed to prove the correctness of the program. This article takes the Greatest number and Find programs as examples to prove their correctness. The methods of snapshot and Logical notation are used to prove the two algorithms to prevent the entry of logic errors. The proof of termination of the algorithm is regarded as an independent exercise. Finally, the two proof methods are summarized.