Proving termination of programs having transition invariants of height omega
italian conference on theoretical computer science(2014)
摘要
We study the proof of a recent and relevant result about termination of programs, the Termination Theorem by Podelski and Rybalchenko [9]. We prove that in a special case, the only case which is used in applications, all programs proved to be terminating may be described by some primitive recursive map. 1 Introducing the Termination Theorem Fix any transition relation R over the set S of possible states of a program P . Assume In ⊆ S is the set of possible initial states of P , and that Acc is the set of accessible states of P , if we start from some state in In and we use the relation R finitely many times. The Termination Theorem by Podelski and Rybalchenko [9] may be stated as follows. The transition relation R is terminating from any initial state if and only if the transitive closure R of R, restricted to the set Acc of accessible states, is included in some finite union of well-founded relations. The authors formulate the Termination Theorem by introducing the concept of “disjunctively well-founded transition invariant”. A disjunctively wellfounded transition invariant is any binary relation T which is the union of a family T1, . . . , Tn of well-founded relations, and which includes the restriction to Acc of R. The original statement of the Termination Theorem is: “R is terminating from any initial state if and only if R has some disjunctively well-founded transition invariant T”. By building over this result the same authors and Byron Cook designed an algorithm they called Terminator [5], checking a sufficient condition for termination for a while-if program P in a simplified programming language. The Terminator algorithm takes P and looks for a disjunctively well-founded transition invariant T = T1 ∪ . . . ∪ Tn for P , with T1, . . . , Tn well-founded relations of height ω. The extra feature “of height ω” is found in the algorithm but not in the Theorem. If the Terminator algorithm finds T1, . . . , Tn as above, it deduces the termination for the program P using the Termination Theorem. This particular application of the Termination Theorem raises an interesting question: what is the status of a transition relation R having a disjunctively well-founded transition invariant T = T1 ∪ . . . ∪ Tnwhere each Ti has height ω? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络