Automatic Termination Analysis of Programs Containing Arithmetic Predicates

For logic programs with arithmetic predicates, showing termination is not easy, since the usual order for the integers is not well-founded. A new method, easily incorporated in the TermiLog system for automatic termination analysis, is presented for showing termination in this case. od consists of the following steps: First, a nite abstract domain for representing the range of integers is deduced automatically. Based on this abn, abstract interpretation is applied to the program. The result is a nite number of atoms abstracting answers to queries which are used to extend the technique of query-mapping pairs. For each query-mapping pair that is potentially non-terminating, a bounded integer-valued termination function is guessed. If traversing the pair decreases the value of the termination function, then termination is established. Simple functions often su ce for each query-mapping pair, and that gives our approach an edge over the classical approach of using a single termination fun...

• Type: Journal
• Year: 2000
• Where: CORR
• Authors: Nachum Dershowitz, Naomi Lindenstrauss, Yehoshua Sagiv, Alexander Serebrenik
• Keywords: Automatic Termination Analysis, CORR 2000, Education, Query-mapping Pairs, Termination Function