一种单路径线性约束的循环程序终止性判断方法

摘要

本发明涉及一种单路径线性约束的循环程序终止性判断方法，包含以下步骤：步骤一、提取出单路径线性约束的循环程序；步骤二、将单路径线性约束的循环程序所转化成的线性不等式系统并求解，无解则该循环程序终止，有解则暂时无法判断其终止性；步骤三、判断线性不等式系统的解中是否存在不动点，存在则该循环程序不终止；如果不存在不动点且状态变量有界，则该循环程序终止，否则无法判断其终止性；步骤四、判断线性不等式系统的解空间的投影是否与循环条件相同，相同则该循环程序不终止，否则无法判断其终止性。该方法通过构造秩函数，采用单量词消去方法，能够在多项式时间内分析出程序的循环终止性，提高了计算效率。