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 )
Would you recommend this review?
Other reviews under "Program Verification": Date
Performance-aware server architecture recommendation and automatic performance verification technology on IaaS cloud
Yamato Y.  Service Oriented Computing and Applications 11(2): 121-135, 2017. Type: Article
Dec 15 2017
Matrix code
Van Emden M.  Science of Computer Programming 843-21, 2014. Type: Article
Aug 27 2014
 Software Fault Interactions and Implications for Software Testing
 IEEE Transactions on Software Engineering 30(6): 418-421, 2004. Type: Article
Sep 9 2005

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright © 2000-2022 ThinkLoud, Inc.
Terms of Use
| Privacy Policy