Automatic Termination Analysis of Programs Containing Arithmetic Predicates

Details Automatic Termination Analysis of Programs Containing Arithmetic Predicates Automatic Termination Analysis of Programs Containing Arithmetic Predicates

2000-11-23

arxiv.org/abs/cs/0011036v1

Computer Science

Programming Languages

Appeared also in Electronic Notes in Computer Science vol. 30

Scientific paper

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. The method consists of the following steps: First, a finite abstract domain for representing the range of integers is deduced automatically. Based on this abstraction, abstract interpretation is applied to the program. The result is a finite 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 suffice for each query-mapping pair, and that gives our approach an edge over the classical approach of using a single termination function for all loops, which must inevitably be more complicated and harder to guess automatically. It is worth noting that the termination of McCarthy's 91 function can be shown automatically using our method. In summary, the proposed approach is based on combining a finite abstraction of the integers with the technique of the query-mapping pairs, and is essentially capable of dividing a termination proof into several cases, such that a simple termination function suffices for each case. Consequently, the whole process of proving termination can be done automatically in the framework of TermiLog and similar systems.

Affiliated with

Also associated with

No associations

Rating

Automatic Termination Analysis of Programs Containing Arithmetic Predicates does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Automatic Termination Analysis of Programs Containing Arithmetic Predicates, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automatic Termination Analysis of Programs Containing Arithmetic Predicates will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-729549