Termination Analysis Of Linear C Loop Code And Tool Development

Terminating analysis of loop programs is an important part of program verification.Ensuring the termination of a loop program is a necessary condition for the correctness of the loop program.At present,the mainstream method used to prove the termination of a program is to prove it by a method of synthesizing a ranking function.Ranking functions maps vector to an element of some well-founded set such that the execution of the updates causes the value of the function to decrease in order.The thesis presents some methods for proving the termination of loop programs by synthesizing complex ranking functions and describes the TermChecker,an automatic verification tool for loop programs.The method for synthesizing the ranking functions is to predefine a so-called template of ranking function first and then try to get the constraints about template parameters.The traditional definition of the ranking function requires that each iteration of the loop decreases the value of the function.Such a constraint is strong,which usually results in no solution to the template parameters.Therefore,in the thesis,we first generalize the concept of traditional ranking function,and propose the concept of k-order ranking function,and prove the termination of the single path linear assignment loop program by synthesizing k-order ranking function.The traditional ranking function is just a special case of the k-rank function.Aiming at the termination of multi-path loop program,the traditional method is proved by synthesizing lexicographic ranking function or global ranking function.However,the existence of lexicographic ranking function or global ranking function for multi-path loop program is only a sufficient condition of terminating multi-path loop program,not a necessary condition.Therefore,in order to further expand the scope of use of the ranking function,we presents a sufficient criterion for termination of multi-path linear assignment loop programs.The criterion is through synthesis the local ranking function to prove the termination of the corresponding loop program.The Experimental results show that for some multi-path linear assignment loop programs which have no global linear ranking functions,lexicographic linear ranking functions,they indeed can be proven to be terminating by our method.In order to achieve the automatic verification of the termination of the loop program,TermChecker has been developed,which can automatically analysis the termination of loop program fragments written in C language.The software first lexical analysis and syntax analysis of the input loop program,and then extract the loop information and pass it to the server.The termination analysis algorithm is written by Maple language.The server call termination analysis algorithm to analyze the loop information,and then send the analysis results to the client.Finally,the client displays the results of the analysis.