论文部分内容阅读
形式化方法是构建可信软件的重要途径.Koch曲线是典型的分形图形,本文使用形式化方法PAR及循环不变式开发策略,开发了基于L系统的Koch曲线非递归算法,并对其进行了形式化的正确性证明.直接面向非递归算法,在得到求解基于L系统的Koch曲线算法的循环不变式的同时,直接得到易读、高效且可靠的非递归算法.对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨.