Original Hoare Logic termination paper

Question

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.

Answer 1

You probably want

• Manna, Pnueli, Axiomatic Approach to Total Correctness of Programs, 1973

Answer 2

There is also a three-page paper by Turing that uses ranking functions to give a correctness proof. His paper is completely readable by modern standards and extremely prescient.

Checking a large routine, Alan Turing, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949.