| Summary: | The ranking function has been extensively studied as an important method of program termination analysis.In this paper,we focus on the termination of single-path loops.Firstly,the concept of two-way iterative loops is proposed,and the single-path loops are divided into bidirectional iterative loops and non-bidirectional iterative loops.Secondly,for the bidirectional iterative loop program,a division method and concept of trivial ranking function are proposed,and it is proved that if a bidirectional iterative loop exists a trivial rank function,it is terminated.As for the non-bidirectional iterative loop,we use incremental function as the division method,i.e.,the original program space is divided into smaller spaces by using incremental function,and the termination of the original program is proved by computing the ranking function on the smaller space.Finally,the problem of computing the trivial ranking function comes down to the SVM classification problem,and we verifies candidate ran-king functions using the tools Z3 or bottema.
|
|---|
