Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
A devil’s advocate against termination of direct recursion
Frühwirth T.  PPDP 2015 (Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, Jul 14-16, 2015)103-113.2015.Type:Proceedings
Date Reviewed: Aug 12 2015

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.

Reviewer:  R. Clayton Review #: CR143682 (1511-0984)
Bookmark and Share
Program Verification (I.2.2 ... )
Concurrent, Distributed, And Parallel Languages (D.3.2 ... )
Constraint And Logic Languages (D.3.2 ... )
Formal Methods (D.2.4 ... )
Program Transformation (I.2.2 ... )
Language Classifications (D.3.2 )
Software/ Program Verification (D.2.4 )
Would you recommend this review?
Other reviews under "Program Verification": Date
Extraction of redundancy-free programs from constructive natural deduction proofs
Takayama Y. Journal of Symbolic Computation 12(1): 29-69, 1991. Type: Article
Oct 1 1992
PROUST: an automatic debugger for PASCAL programs
Johnson W., Soloway E. BYTE 10(4): 179-190, 1985. Type: Article
Aug 1 1985
Breeding software test cases with genetic algorithms
Berndt D., Fisher J., Johnson L., Pinglikar J., Watkins A.  Conference on System Sciences (Proceedings of the 36th Annual Hawaii International Conference on System Sciences (HICSS’03) - Track 9, Big Island, HI, Jan 6-9, 2003)338.12003. Type: Proceedings
Jun 3 2004

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy