在 Hoare logic ，人们经常区分部分正确性和完全正确性。部分正确意味着程序满足其规范，或者不会终止(无限循环或递归)。
有谁知道为什么要引入这种关于终止的微妙之处？对我来说，似乎只有完全正确才有用:程序满足其规范并终止。谁想要执行可能无限循环？
最佳答案
我们谈论部分正确性这一事实并不意味着证明部分正确性同样有用。我们谈论部分正确性是因为我们有一种证明它的技术(霍尔逻辑)，并且我们应该了解该技术的局限性。
霍尔逻辑可用于证明算法永远不会以错误结果终止(部分正确)，但不能用于证明算法总是以正确结果终止(完全正确)。这些在逻辑上并不等价，但如果我们没有单独的术语来表示它们，那么很容易天真地认为它们是等价的。
Using standard Hoare logic, only partial correctness can be proven, while termination needs to be proved separately.
考虑霍尔三元组的一种方法是，它是一段代码，用两个 assertions 注释。 ，一个在该段之前，一个在该段之后。断言是一种逻辑测试，当达到断言时，要么通过，要么失败。霍尔三元组表示，如果第一个断言永远不会失败，那么第二个断言也永远不会失败。
从根本上讲，您不能编写一个断言来表示将达到一行代码，因为无论您编写什么条件，如果从未达到，则断言永远不会失败。
请注意，您可以 assert false 表示不会到达某行代码，但 assert true 永远不会失败，无论是否成功曾经达到过。
因此，虽然霍尔逻辑的证明能够得出算法中的最终断言(即其后置条件)永远不会失败的结论，但这并不意味着算法终止。
关于algorithm - 为什么是部分正确而不是完全正确？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/51768952/