我正在尝试证明以下算法以查看是否存在从 u 到 v 的图 G = (V,E) 中的路径。
我知道要完成证明，我需要证明终止、不变量和正确性，但我不知道如何证明。我想我需要在 while 循环中使用归纳法，但我不确定如何使用。
我如何证明算法的这三个特征？
最佳答案
免责声明:我不知道你希望你的证明有多正式，我也不熟悉正式证明。
- while 循环归纳:一开始是真的吗？它在一个步骤之后是否仍然为真(非常简单的路径属性)？
- 同样的想法，对k的归纳(为什么是k+1？？？):一开始是真的吗？它在一个步骤之后是否仍然为真(非常简单的路径属性)？
- 将 Reach 视为一个严格递增的集合。
终止:也许您可以使用与图形直径相关联的非常简单的属性？
(这个问题可能在别处得到更好的回答，也许在 https://cstheory.stackexchange.com/ 上？)
关于algorithm - 证明图上的广度优先遍历，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/23464469/