# 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]|<dmin

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

return dmin

• Hint: you could fix i and dmin, and prove using a loop invariant that after the inner loop dmin has the minimum value among min_i = {dmin,dist(A[i],A[0]),dist(A[i],A[1],...}. Then using that prove for the outer loop that dmin holds the minimum value among {min_1, min_2,...} – Odo Frodo May 13 '18 at 2:04

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.