CODEWITHSUNDEEP
loop-invariant
Wobblester
Wobblester

Reputation: 740

Correct loop invariant?

I am trying to find the loop invariant in the following code:

Find Closest Pair Iter(A) :

# Precondition: A is a non-empty list of 2D points and len(A) > 1. 

# Postcondition: Returns a pair of points which are the two closest points in A.
    min = infinity
    p = -1
    q = -1
    for i = 0,...,len(A) - 1:`=
        for j = i + 1,...,len(A) - 1:
             if Distance(A[i],A[j]) < min:
                 min = Distance(A[i],A[j])
                 p = i
                 q = j
    return (A[p],A[q])

I think the loop invariant is min = Distance(A[i],A[j]) so closest point in A is A[p] and a[q] . I'm trying to show program correctness. Here I want to prove the inner loop by letting i be some constant, then once I've proven the inner loop, replace it by it's loop invariant and prove the outer loop. By the way this is homework. Any help will be much appreciated.

Upvotes: 1

Views: 608

Answers (1)

Marcelo Zabani
Marcelo Zabani

Reputation: 2279

I'm not sure I fully understand what you mean by replacing the inner loop by its loop invariant. A loop invariant is a condition that holds before the loop and after every iteration of the loop (including the last one).
That being said, I wouldn't like to spoil your homework, so I'll try my best to help you without giving too much of the answer away. Let me try:

There are three variables in your algorithm that hold very important values (min, p and q). You should ask yourself what is true about these values as the algorithm goes through each pair of points (A[i], A[j])?

In a simpler example: if you were designing an algorithm to sum values in a list, you would create a variable called sum before the loop and assign 0 to it. You would then sum the elements one by one through a loop, and then return the variable sum.
Since it is true that this variable holds the sum of every single element "seen" in the loop, and since after the main loop the algorithm will have "seen" every element in the list, the sum variable necessarily holds the sum of all values in the list. In this case the loop invariant would be: The sum variable holds the sum of every element "seen" so far.

Good luck with your homework!

Upvotes: 0

Related Questions