 By Hoare’s own admission in Hoare [1979], his original calculus was merely a starting point and suffered quite a few limitations. Particularly, it only allows one to reason about partial correctness. That is, the truth of a statement {A}α{B} only makes sure that all executions of α starting in a state satisfying A will end in a state satisfying B, or will not halt. That is, a partially correct program may have non-terminating executions. (In fact, a program that has no terminating execution will always be partially correct. This is the case for example of the program while 1 do skip. The formula A → [while 1 do skip]B is deducible for all formulas A and B.) The calculus offers no basis for a proof that a program terminates. It can be modified so as to account for total correctness of programs: partial correctness plus termination. It is achieved by amending the rule of iteration. We do not present it here and refer the interested reader to Apt [1981].