嵌套循环不变式如何处理内外循环

如何找到一个嵌套循环的两个不变式

代码如下

def SCSLength(X, Y):

m = len(X)
n = len(Y)

# lookup table stores solution to already computed subproblems
# i.e., `T[i][j]` stores the length of SCS of substring
# `X[0…i-1]` and `Y[0…j-1]`
T = [[0 for x in range(n + 1)] for y in range(m + 1)]

# initialize the first column of the lookup table
for i in range(m + 1):
    T[i][0] = i

# initialize the first row of the lookup table
for j in range(n + 1):
    T[0][j] = j

# fill the lookup table in a bottom-up manner
for i in range(1, m + 1):
    for j in range(1, n + 1):

        # if the current character of `X` and `Y` matches
        if X[i - 1] == Y[j - 1]:
            T[i][j] = T[i - 1][j - 1] + 1

        # otherwise, if the current character of `X` and `Y` don't match
        else:
            T[i][j] = min(T[i - 1][j] + 1, T[i][j - 1] + 1)

# SCS will be the last entry in the lookup table
return T[m][n]

是否应该先处理内循环还是外循环， 我做的是：At the beginning of the jth iteration of the inner for loop,

T [i][j − 1] is the length of the shortest common supersequence that contains the first
ith and (j − 1)th elements in X and Y respectively. 但是没办法证明第二部。