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.
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."