该文研究的主要目标是利用薛教授在开发循环不变式的新策略中提出的递归定义思想,探索一类递归定义问题的循环不变式开发技术,并应用于涉及组合数据结构的复杂算法程序的形式化推导和证明.具体研究成果如下:1.进一步深入研究了循环不变式在算法程序形式化方法中的地位和作用;2.对现有循环不变式开发技术进行了分析和比较,剖析了其难以实用的原因;3.基于现有循环不变式开发技术中的递归定义思想,提出了开发复杂递归问题循环不变式的两种新策略;4.利用抽象程序设计语言Apla精确描述了6个典型树、图等问题的程序规约和求解算法程序,用上述提出的两种新策略开发了循环不变式,实现了严格的形式化推导或证明,并用PAR方法提供的算法程序自动转换系统将得到的Apla算法程序转换成对应的Delphi和C<++>程序,均得到了正确的运行结果,大幅度地提高了这类复杂算法程序的可靠性和开发效率.总之,该文得到的结果可应用于一类复杂算法程序的形式推导和证明,方法简单,应用方便,为实现算法设计的形式化和自动化作出了有效的贡献.