Why partial correctness instead of total correctness?

Question

In Hoare logic, one often makes a distinction between partial and total correctness. Partial correctness means that the program fulfills its specification, or does not terminate (infinite loop or recursion).

Does anyone know why this subtlety about termination was introduced ? To me it seems only total correctness is useful : a program fulfills its specification and terminates. Who wants to execute a possibly infinite loop ?

Answer 1

While many termination cases can be addressed with a minor augmentation of the Hoare logic, and more can be rewritten to be so addressed, this is not true of all cases.

Thus, in the general case, you may need to use an elaborate proof construction to prove total correctness. This should be more than sufficient to justify making a distinction between partial and total correctness.

To look at it another way: when proving termination is much more difficult than proving partial correctness, a practical engineering approach should consider whether the additional effort is worth it.

Answer 2

The fact that we talk about partial correctness doesn't mean partial correctness is equally useful to prove. We talk about partial correctness because we have a technique for proving it (Hoare logic), and we should understand the limitations of that technique.

Hoare logic can be used to prove that an algorithm never terminates with an incorrect result (partial correctness), but it cannot be used to prove that an algorithm always terminates with a correct result (total correctness). These are not logically equivalent, but if we didn't have separate terms for them then it would be easy to naively assume they are equivalent.

Says Wikipedia:

Using standard Hoare logic, only partial correctness can be proven, while termination needs to be proved separately.

One way to think of a Hoare triple is that it is a segment of code, annotated with two assertions, one before the segment and one after it. An assertion is a logical test which either passes or fails when the assertion is reached. The Hoare triple says that if the first assertion never fails, then the second assertion also never fails.

Fundamentally, you cannot write an assertion which says that a line of code will be reached, because whatever condition you write, the assertion never fails if it is never reached. Note that you can assert false to say that a line of code won't be reached, but assert true never fails, whether or not it is ever reached. Therefore, although a proof by Hoare logic is able to conclude that the final assertion in an algorithm (i.e. its postcondition) never fails, that doesn't imply the algorithm terminates.