Would "there exists a pair x,y in the subarray arr[left:right+1] that sums up to k." be a good loop variant for the code below which determines given a sorted array of integers if there is a a pair of integers, x and y, that sum to k.

The code:

def has_interesting_pair(arr, k):
    left, right = 0, len(arr) - 1

    while left < right:
        current_sum = arr[left] + arr[right]

        if current_sum == k:
            return True
        elif current_sum < k:
            left += 1
        else:
            right -= 1

    # If no interesting pair is found
    return False

I wanted to check if this was the best possible loop variant that could be used to prove iterative correctness also because this assumes that the pair exists because it could also not exist.

3

There are 3 best solutions below

0
On

You correctly observe that there might not be a suitable sum in the array.

Just after the while I recommend you write a variant comment: "if it exists, the required sum falls within the interval left..right inclusive, and that interval shrinks with each iteration."

0
On

As an example, you could approach the problem differently (after all, if i + j == k, then k - i == j):

def has_interesting_pair(arr, k):
    for i in [k - left for left in arr if (k - left) >= left]:
        if i in arr:
            return True
    else:
        return False
0
On

Given that the sum will be composed of a small and a larger (or equal) number, you could break the loop earlier when either the left side is greater than half the target or the right side is less than half.

for example:

if arr[left]  * 2 > k : break
if arr[right] * 2 < k : break

This would be a small optimization that only applies to specific patterns of data, and in practice it may add more overhead than it saves time, but in terms of iterations, it would be a little more efficient.