Total Correctness

A total correctness statement in Hoare Logic or Separation Logic is a triple $\Hoare{P}{C}{Q}$ that states that a program $C$ that starts in a state $P$ must terminate in a state satisfying $Q$.