当今时代,计算机已经成为人们工作生活必不可少的工具。计算机及其软件使用已经渗透到人类活动的各个领域,软件作为计算机功能实现的核心要素,使得设计高可信软件成为计算机领域日益关注的问题。而软件验证作为高可信软件设计的重要部分,实现软件程序的自动验证将对高可信软件设计工作具有十分重要的意义。　　作为计算机程序设计领域的传统研究课题,程序验证是研究程序正确性的理论。程序终止性问题是程序验证的主要内容,程序终止性问题的研究突破对程序验证工作起到十分关键的作用。　　本文主要研究了程序的终止性问题,在基于特征值的理论中提出了一类非线性的while型循环程序的终止性是可以判定的,指出该类程序的终止性与其赋值矩阵的正特征值相对应的特征向量有关,并提出判定此类程序终止性的一种新方法,既能判定程序是否终止,又能对不是所有初始值均终止的程序给出终止情况下的初始值建议。　　文章首先简要介绍程序完全正确性的定义,程序的完全正确性是由程序的部分正确性和程序的终止性构成。再分别对程序的部分正确性和终止性的判定方法进行论述:　　(1)关于程序的部分正确性。　　列举不变式断言,Hoare公理化和Dijkstra最弱前置谓词变换三种判定程序部分正确性的方法。　　(2)关于程序的终止性。　　①指出多数程序终止性证明方法所采用的本质思想是判定程序迁移关系是良基关系的方法;　　②讨论基于秩函数的线性循环程序终止性分析和基于特征值理论的线性循环程序终止性分析两种方法,归纳两种方法的原理、缺陷及优势,并举出两种方法合适的线性循环程序。　　③讨论基于不动点定理的非线性循环程序终止性分析、基于特征值理论的非线性循环程序终止性分析和基于有限差分的非线性循环程序终止性分析三种方法。归纳三种方法的原理、缺陷及优势,并举出三种方法适合的非线性循环程序。　　最后,归纳总结代数方法验证程序终止性的一般步骤,指出程序终止性判定方法的未来研究发展方向。