| 形式化开发非递归Koch曲线算法 |
| |
| 引用本文： | 刘润杰,申金媛,穆维新.形式化开发非递归Koch曲线算法[J].计算机科学,2011,38(9):126-129. |
| |
| 作者姓名： | 刘润杰 申金媛 穆维新 |
| |
| 作者单位： | (郑州大学信息工程学院 郑州 450001) |
| |
| 基金项目： | 本文受河南省教育厅自然科学研究计划项目((2010A510015,2008B120010),江酉省高性能计算技术重点实验室开放课题资助 |
| |
| 摘 要： | 形式化方法是构建可信软件的重要途径。Koch曲线是典型的分形图形。基于形式化方法PAR及循环不变式开发策略，开发了Koch曲线非递归算法，并对其进行了形式化的正确性证明。在得到求解Koch曲线算法的循环不变式的同时，直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发策略开发分形程序非递归算法作了较深入的实践和探讨。
|
| 关 键 词： | Koch曲线，形式化方法，非递归，PAR方法，循环不变式 |
Formal Development of Non-recursive Algorithm for Koch Curve |
| |
| LIU Run-jie,SHEN Jin-yuan,MU Wei-xin.Formal Development of Non-recursive Algorithm for Koch Curve[J].Computer Science,2011,38(9):126-129. |
| |
| Authors: | LIU Run-jie SHEN Jin-yuan MU Wei-xin |
| |
| Affiliation: | (Schools of Information Engineering,Zhengzhou University,Zhengzhou 450001,China) |
| |
| Abstract: | 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 dvcloped, 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. |
| |
| Keywords: | Koch curve Formal method Non-recursive PAR method Loop invariant |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
