形式化开发基于L系统的Koch曲线算法

摘要：

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

关键词： 软件开发 Koch曲线 形式化方法 L系统 循环不变式

作者: 刘润杰 文政 申金媛 穆维新

作者单位: 郑州大学信息工程学院,河南郑州 450001

会议类型: 国内会议

会议名称: 2012河南省计算机大会暨学术年会

会议地点: 开封

会议语种:中文

页码: 130-134

在线出版日期: 2012-08-01（万方平台首次上网日期，不代表论文的发表时间）