A totally correct system terminates. Instead of establishing termination directly, this paper describes a technique based on non-termination. This technique is statically derivable from the program text and produces non-termination results that are informative relative to the system’s failure to terminate.

A logically adept reader may be feeling anxious: to show not non-terminating is not to show termination. The logically sophisticated reader may be anticipating restrictive table setting to support this technique. The technique is described relative to a rule-based constraint language. “Devil’s rules,” syntactically derived from a program’s directly recursive rules, are added to the program, and are designed to drive the program into non-termination, called maximally vicious computations. The central theorem of the paper shows that non-terminating programs contains maximally vicious computations characterized by devil’s rules. In the absence of devil’s rules, a program terminates.

Now for the fine print: a program with devil’s rules may converge to failure, from which nothing can be concluded. In addition, the technique applies only to programs with rules satisfying various conditions needed by devil’s-rule derivations. The technique is in its early days, however, and further work may broaden and strengthen the results it can achieve.

The paper is a vigorous read, requiring knowledge of more advanced forms of logic programming as well as the usual first-order predicate logic. The simple even-predicate running example proved to be a surprisingly effective help when working through the paper carefully.