在Hoare逻辑中，人们经常区分部分正确性和完全正确性。部分正确性意味着程序满足其规范，或者不终止(无限循环或递归(。
有谁知道为什么引入这种关于终止的微妙之处？对我来说，似乎只有完全正确才有用：程序满足其规范并终止。谁想执行一个可能的无限循环？
我们谈论部分正确性并不意味着部分正确性同样有用。我们谈论部分正确性，因为我们有一种证明它的技术(霍尔逻辑(，我们应该了解该技术的局限性。
Hoare逻辑可用于证明算法永远不会以不正确的结果终止(部分正确性(，但不能用于证明算法总是以正确的结果终止(完全正确性(。这些在逻辑上不是等价的，但是如果我们没有单独的术语，那么很容易天真地假设它们是等价的。
维基百科说：
使用标准的Hoare逻辑，只能证明部分正确性，而终止需要单独证明。
考虑Hoare三元组的一种方法是，它是一段代码，用两个断言注释，一个在段之前，一个在段之后。断言是一种逻辑测试，在达到断言时通过或失败。Hoare三重说，如果第一个断言永远不会失败，那么第二个断言也永远不会失败。
从根本上说，你不能写一个断言说将达到一行代码，因为无论你写什么条件，如果从未达到断言，断言永远不会失败。 请注意，你可以assert false说一行代码不会被触及，但assert true永远不会失败，无论它是否被达到。 因此，尽管Hoare逻辑的证明能够得出结论，算法中的最终断言(即其后置条件(永远不会失败，但这并不意味着算法终止。
虽然许多终止情况可以通过对Hoare逻辑的微小增强来解决，并且可以重写更多情况来解决，但并非所有情况都是如此。
因此，在一般情况下，您可能需要使用精心设计的证明结构来证明完全正确。 这应该足以证明区分部分正确和完全正确是合理的。
换个角度看：当证明终止比证明部分正确性困难得多时，实用的工程方法应该考虑额外的努力是否值得。