# 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),dist(A[i],A,...}. 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

## 1 Answer

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.

• Thank you. But I don't really understand what you mean. Can you please provide some assertions for this algorithm?<br/> (something like if i≠j and |A[i]-A[j]|<dmin {i !=j and 0<i<n-1 and 0<j<n-1 and |A[i]-A[j]|<dmin} if condition true)<br/> – chester713 May 12 '18 at 2:26