algorithm - 为什么部分正确而不是完全正确？

Question

在霍尔逻辑中，人们经常区分部分正确性和完全正确性。部分正确性意味着程序满足其规范，或者不会终止（无限循环或递归）。

有谁知道为什么要引入这种关于终止的微妙之处？对我来说，似乎只有完全正确才有用：程序满足其规范并终止。谁想执行一个可能的无限循环？

Answer 1

我们谈论部分正确性这一事实并不意味着部分正确性对证明同样有用。我们谈论部分正确性是因为我们有一种证明它的技术（霍尔逻辑），我们应该了解这种技术的局限性。

霍尔逻辑可用于证明算法永远不会以不正确的结果终止（部分正确性），但不能用于证明算法总是以正确的结果终止（完全正确性）。这些在逻辑上不是等价的，但如果我们没有单独的术语，那么很容易天真地假设它们是等价的。

维基百科说：

使用标准的霍尔逻辑，只能证明部分正确性，而终止需要单独证明。

考虑 Hoare 三元组的一种方法是，它是一段代码，用两个断言注释，一个在段之前，一个在段之后。断言是一个逻辑测试，当达到断言时它要么通过，要么失败。Hoare 三元组表示，如果第一个断言永远不会失败，那么第二个断言也永远不会失败。

从根本上说，你不能写一个断言将达到一行代码，因为无论你写什么条件，如果从未达到，断言永远不会失败。请注意，您可以assert false说一行代码不会被访问，但assert true永远不会失败，无论它是否曾经被访问过。因此，尽管 Hoare 逻辑的证明能够得出结论，算法中的最终断言（即其后置条件）永远不会失败，但这并不意味着算法终止。

Answer 2

虽然可以通过对 Hoare 逻辑的少量扩充来解决许多终止情况，并且可以重写更多以解决问题，但并非所有情况都如此。

因此，在一般情况下，您可能需要使用复杂的证明结构来证明完全正确。这应该足以证明区分部分正确性和完全正确性是合理的。

换个角度来看：当证明终止比证明部分正确性要困难得多时，实用的工程方法应该考虑额外的努力是否值得。