I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by that I mean a HL for a C-like toy language).
I've had a look at Axiomatic basis for Computer Programs (PDF) (which seems to be essentially Hoare logic of the partial correctness flavour) and A note on the for rule, which mentions proof of a while rule, but can't seem to find the missing link; a paper on termination/the while rule/Total correctness.