摘要
形式化方法是构建可信软件的重要途径。Koch曲线是典型的分形图形。基于形式化方法PAR及循环不变式开发策略,开发了Koch曲线非递归算法,并对其进行了形式化的正确性证明。在得到求解Koch曲线算法的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨。
Formal method is an important approach for construction of the trustworthy software.Koch curve is one of the typical fractals.A non-recursive algorithmic program of Koch curve was dveloped,employing PAR method and the strategy of developing loop invariant and the algorithm was verified formally.This paper achieved loop invariant of Koch curve with readable,efficient and reliable non-recursive algorithm finally.The paper contributed to developing non-recursive algorithm using formal method and new strategy of developing loop invariant.
出处
《计算机科学》
CSCD
北大核心
2011年第9期126-129,共4页
Computer Science
基金
河南省教育厅自然科学研究计划项目(2010A510015
2008B120010)
江西省高性能计算技术重点实验室开放课题资助
