2
$\begingroup$

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
$\endgroup$
  • $\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 '18 at 2:04
1
$\begingroup$

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.

$\endgroup$
  • $\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 '18 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.