A closer look at termination

Summary Several methods for proving that computer programs terminate are presented and illustrated. The methods considered involve (a) using the no-infinitely-descending-chain property of well-founded sets (Floyd's approach), (b) bounding a counter associated with each loop (loop approach), (c) showing that some exit of each loop must be taken (exit approach), or (d) inducting on the structure of the data domain (Burstall's approach). We indicate the relative merit of each method for proving termination or non-termination as an integral part of an automatic verification system.