Proving the correctness of brute force maximum sub array algorithm

Question

I am trying to prove the correctness of the brute force version of the maximum sub array problem given below:

def max_subarray_bf(lst):
    left = 0
    right = 0
    max = lst[0]
    for i in range(len(lst)):
        current_sum=0
        for j in range(i, len(lst)):
            current_sum+=lst[j]
            if current_sum>max:
                max=current_sum
                left=i
                right=j
    return (left, right, max)

but I seem to be stuck at designing the loop invariant, that might be because the inner loop changes a global variable(max) which makes it hard for me to portray what (max) represents in a loop invariant corresponding to the inner loop.

My attempt:

Overall the algorithm works by finding the maximum sub array of the following sub arrays:

{[0],[0,1],...,[0,...,n]

 [1],[1,2],...,[1,...,n]

 .

 .

 .

 [n]}

• Inner Loop Invariant:
  • Current_sum is the sum of all elements in the array [i...j]
  • Stuck here as I can't seem to capture what max would be in terms of i and j, and consequently left and right