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


for i←0 to n-1 do

    for j←0 to n-1 do

        if i≠j and |A[i]-A[j]|<dmin


return dmin
  • $\begingroup$ 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,...} $\endgroup$
    – Odo Frodo
    May 13, 2018 at 2:04

1 Answer 1


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.

  • $\begingroup$ 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/> $\endgroup$
    – chester713
    May 12, 2018 at 2:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.