迪杰斯特拉正确性证明

迪杰斯特拉算法的正确性可以通过以下步骤进行证明：

1. 初始化：将起始节点标记为已访问，并将其距离设置为0。对于其他节点，将其距离设置为无穷大。

2. 选择最小距离节点：从未访问的节点中选择一个距离最小的节点，将其标记为已访问。

3. 更新相邻节点的距离：对于与当前节点相邻的节点，如果通过当前节点到达该节点的距离小于该节点当前的距离，则更新该节点的距离。

4. 重复步骤2和步骤3，直到所有节点都被访问。

证明：

首先，我们证明属性1：对于起始节点s，D[s] = 0。这是因为我们将起始节点的距离初始化为0。

然后，我们证明属性2：对于任意节点v，如果v被标记为已访问，则D[v]是从起始节点s到节点v的最短路径的长度。我们可以通过反证法来证明。假设存在一个节点v，它被标记为已访问，但存在一个更短的路径从起始节点s到节点v。这意味着存在一个节点u，它是路径上的前一个节点，并且D[u] + weight(u, v) < D[v]。但是，根据算法的步骤3，我们会更新节点v的距离为D[u] + weight(u, v)，这与假设矛盾。

最后，我们证明属性3：对于任意节点v，如果v被标记为已访问，则从起始节点s到节点v的最短路径是通过已访问的节点构成的。我们可以通过反证法来证明。假设存在一个节点v，它被标记为已访问，但存在一个更短的路径从起始节点s到节点v，该路径不经过已访问的节点。这意味着存在一个节点u，它是路径上的前一个节点，并且D[u] + weight(u, v) < D[v]。但是，根据算法的步骤2，我们会选择距离最小的节点作为下一个访问节点，而不会选择节点v。因此，不存在这样的路径，与假设矛盾。

综上所述，迪杰斯特拉算法的正确性得到证明。