My question is about how to prove the correctness of this algorithm, I know it is not a good algorithm, it is not efficient and can be improved. How could I prove it still returns the desired value? What are the loop invariant and variant? How to insert assertions between lines?
The algorithm goes like following,
Algorithm MinDistance (A [0…n-1])
//Input: Array A [0...n-1] of numbers //Output: Minimum distance between two of its elements dmin←∞ for i←0 to n-1 do for j←0 to n-1 do if i≠j and |A[i]-A[j]|<dmin dmin←|A[i]-A[j]| return dmin