Electronic Resource
Springer
Acta informatica
5 (1975), S. 333-352
ISSN:
1432-0525
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
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.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/BF00264565
Permalink
| Library |
Location |
Call Number |
Volume/Issue/Year |
Availability |
