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 ?
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.