How to prove the correctness of the MinDistance algorithm? 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]|&lt;dmin

        dmin←|A[i]-A[j]|

return dmin
Define an order of pairs of indices $(i,j)$ according to the order in which they are accessed in your code. At the end of the $(i,j)$th iteration, $dmin$ holds the minimum of $|A(k)-A(\ell)|$ among all pairs $(k,\ell) \preceq (i,j)$ such that $k \neq \ell$. This loop invariant is easy to prove, and implies the correctness of the entire algorithm.