部分正確性與完全正確性（partial vs total correctness）

對一個程式，你可能做出兩種不同的承諾。較弱的：「若它停下來，答案就是對的。」較強的：「它會停下來，而且答案是對的。」兩者之間的差距，就是程式可能永遠跑下去的那個可能性。部分正確性只涵蓋第一個承諾；完全正確性再加上「程式真的會停機」這個保證。一個永遠迴圈的程式，弔詭地說是部分正確的（它從不給出錯誤答案，因為它根本不給任何答案），但毫無用處——這正是我們通常想要完全正確性的原因。

精確地說：給定一個前置條件（對輸入的假設）與一個後置條件（輸出應滿足的性質），部分正確性說「只要前置條件成立且程式終止，後置條件就成立」。完全正確性說「只要前置條件成立，程式就會終止且後置條件成立」。這兩個證明乾淨地一分為二：迴圈不變量／歸納法論證確立部分正確性（離開時結果正確），而另一個良基終止度量則確立離開總會發生。兩者合起來給出完全正確性。所以完全正確性 = 部分正確性 + 終止。

把這兩者分清楚在實務上很重要。許多正確性說明悄悄只證了部分正確性而忘了終止——對你已知會停的程式沒問題，對可能不會停的程式則危險。反過來，你也可能有終止卻沒有正確性（一個總會停、卻停在錯誤答案的程式）。在某些情境（反應式系統、伺服器）你其實想要不終止，於是「完全正確性」會用其他性質重新表述。乾淨的結論：不變量證明迴圈結束時答案正確；度量證明迴圈會結束；要完整保證，兩者都需要。