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
Improve this question
$\endgroup$
1
  • $\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
    Commented May 13, 2018 at 2:04

1 Answer 1

Reset to default
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.

Improve this answer
$\endgroup$
1
  • $\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
    Commented May 12, 2018 at 2:26

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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