随着计算机的发展,软件在各行各业已扮演着越来越重要的角色。自2007年“可信软件基础研究”重大研究计划启动以来,我国投入了大量的科研经费,其中可信软件相关开发工具及其支撑平台、可信软件的构造及验证是该研究计划的主要目标。算法是计算机软件的灵魂,对非线性复杂结构(如树、图)算法的研究一直是国内外研究的热点。树形结构是一种典型的非线性数据结构,它能够支持强大的搜索算法、有效的分配内存空间和提供有规则的数据存储,对树形结构算法的开发与验证是软件形式化、可信软件研究领域的一个挑战性问题。二叉树最具代表性,大部分利用二叉树结构处理的算法不仅写起来简单,而且运行效率更高。二叉树算法的应用领域非常广泛,如数据解压、信息加密、内存管理、网络通信和集群计算等等。二叉树算法可以是递归和非递归的,其中递归算法递归调用的成本高(额外的堆栈空间分配和多函数调用)且危险(堆栈溢出),在关键任务(如航空、NASA探测车)的系统编程中,递归调用是完全禁止的。而非递归算法效率更高,因而开发高可靠的二叉树非递归算法尤为重要。本文结合PAR方法和交互式定理证明工具Isabelle对三类典型的二叉树算法进行开发和机器辅助证明。该方法不仅克服了传统手工验证的繁琐性和易错性,而且大幅度提高了所开发出算法程序的可靠性和可信性。若干实例开发与验证的成功,说明了该方法的有效性和可行性。本文的主要工作包括:1.提出了一种结合PAR方法和交互式定理证明器Isabelle对二叉树算法进行开发和机器辅助证明的方法。经PAR方法开发的算法是非递归的,提高了算法效率;开发后的算法经过机器辅助证明,不仅克服了传统手工验证的繁琐性和易错性,而且大幅度提高了所开发出算法程序的可靠性和可信性。2.通过归纳分析二叉树算法的循环不变式组成结构和输出属性特征,将二叉树算法分成三大类,通过发现每类算法之间的共性,十分有利于简化开发和验证的过程。3.成功的开发和验证了一系列二叉树非递归算法,包括:二叉树前序、中序、后序、层次遍历,求二叉树内部路径长度,交换二叉树所有结点的左右子女,二叉排序树的增删改查操作,判断二叉树是否为满二叉树,判断二叉树是否为平衡二叉树等。这是首次形式化验证一系列非递归的高效二叉树算法。4.在此基础上,使用Isabelle定义了常用二叉树数据结构的数据类型、相关操作和辅助函数,形成二叉树算法定理证明库,有利于将来复用,构造更加复杂的验证。