我想为下面的代码找到一个循环不变式，我似乎无法弄清楚这段代码中呈现的任何关系。
该算法的目标是找到二叉树中所有元素的总和。它将节点存储在名为s的堆栈中。
def TreeSum(root):
res = 0
s.push(root)
while s.size > 0:
node = s.pop()
res = res + node.num
if node.right != None:
s.push(node.right)
elif node.left != None:
s.push(node.left)
return res
我注意到res是当前节点的所有父节点以及其父节点左侧的父节点的总和，但是我不知道如何将其表达为循环不变式。
该算法应用于计算二叉树中数字的总和。为了证明其正确性，有两个重要事实需要证明：首先，它确实计算了它访问的节点的总和；其次，它访问了每个节点一次。因此，我们将需要至少找到两个不变量，一个用于证明每个事实。
为了更正式地讨论“已访问”或“未访问”节点，让我们在算法中添加几行内容，以跟踪“已访问”节点的列表。这些行显然不会改变算法的行为，因为visited仅被写入，从不读取：
def TreeSum(root):
res = 0
s = Stack()
s.push(root)
visited = [] # added line to simplify proof
while s.size > 0:
node = s.pop()
visited.append(node) # added line to simplify proof
res = res + node.num
if node.right != None:
s.push(node.right)
elif node.left != None:
s.push(node.left)
return res
我还添加了该算法必需的 行，以使s为新堆栈，否则未定义s或一个全局变量，那么我们不能保证算法启动时为空。
所需的不变式如下：
res等于a.num中a in visited的总和。a in visited的所有子节点c not in visited和所有节点a，c in s或唯一的节点b in s使得{ {1}}是b的后代和a的祖先。c或root in s。需要第三个不变量得出结论，root in visited包含循环终止时的每个节点，因此visited是每个节点的总和。没有这个，当res为空且visited为0时，其他两个不变量将得到满足，但是第三个不变量使我们可以拒绝这种可能性。