<p>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. </p>

<blockquote>
  <p><a href="http://www.turingarchive.org/browse.php/B/8" rel="nofollow">Checking a large routine</a>, Alan Turing, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949.</p>
</blockquote>

CC BY-SA 3.0
2012-10-16T02:55:33.873Z
2012-10-16T02:55:33.873Z
Vijay D
<p>You probably want</p>

<ul>
<li>Manna, Pnueli, <a href="https://www.google.co.uk/search?q=Axiomatic%20approach%20to%20total%20correctness%20of%20programs%20stanford%20pdf">Axiomatic Approach to Total Correctness of Programs</a>, 1973</li>
</ul>

CC BY-SA 3.0
2012-10-07T14:37:44.783Z
2012-10-07T14:37:44.783Z
Radu GRIGore
<p>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). </p>

<p>I've had a look at <a href="http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf"><em>Axiomatic basis for Computer Programs</em></a> (PDF) (which seems to be essentially Hoare logic of the partial correctness flavour) and
<em>A note on the for rule</em>, 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.</p>

<reference-request><lo.logic><pl.programming-languages><program-verification><program-logic>
Original Hoare Logic termination paper
C.E.Sally
# Original Hoare Logic termination paper

(Asked by: username_0 on 2012-10-07)

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*](http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf) (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.

**Tags:** reference-request, lo.logic, pl.programming-languages, program-verification, program-logic


---

## 2 answers

### Answer by username_2 on 2012-10-07. Score: 13 | Accepted answer

You probably want

* Manna, Pnueli, [Axiomatic Approach to Total Correctness of Programs](https://www.google.co.uk/search?q=Axiomatic%20approach%20to%20total%20correctness%20of%20programs%20stanford%20pdf), 1973


---

### Answer by username_1 on 2012-10-16. Score: 4

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](http://www.turingarchive.org/browse.php/B/8), Alan Turing, Report of a Conference on High Speed Automatic Calculating Machines, pp.67-69, 1949.


---

