8
$\begingroup$

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.

$\endgroup$
13
$\begingroup$

You probably want

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.