python - 二叉树和的循环不变量

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是所有当前节点的父节点及其父节点左侧的总和，但我不知道如何将其表述为循环不变量。

标签： pythonproofcorrectnessloop-invariantproof-of-correctness

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.numfor的总和a in visited。
2. 对于所有节点a in visited，以及c not in visited作为 的后代的所有节点a，c in s或者有一个唯一的节点b in s，它b是 的后代a和祖先c。
3. 要么root in s要么root in visited。

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