二叉树和的循环不变量

Question

我想为下面这段代码找到一个循环不变量，我似乎无法弄清楚这段代码中呈现的任何类型的关系。

此算法的目标是找到二叉树中所有元素的总和。它将节点存储在一个名为 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 是所有当前节点的父节点及其父节点左侧的总和，但我不知道如何将其表述为循环不变量。

Answer 1

这个算法应该计算二叉树中数字的总和。为了证明它的正确性，有两个重要的事实需要证明：首先它确实计算了它访问的节点的总和，其次它访问了每个节点一次。因此，我们需要找到至少两个不变量，一个用于证明这些事实。

为了更正式地讨论“已访问”或“未访问”节点，让我们在算法中添加几行代码，以跟踪“已访问”节点列表。这些行显然不会改变算法的行为，因为 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 没有定义或者如果它是一个全局变量，那么我们不能保证算法开始时它是空的。

需要的不变量如下：

1. res 等于 a.num 与 a in visited 的总和。
2. 对于所有节点a in visited，以及作为a 后代的所有节点c not in visited，c in s 或存在唯一节点b in s 使得b 是a 的后代，并且c 的祖先。
3. root in s 或 root in visited。

需要第三个不变量来推断visited 包含循环终止时的每个节点，因此res 是每个节点的总和。没有这个，当visited 为空且res 为0 时，其他两个不变量得到满足，但第三个不变量允许我们拒绝这种可能性。