形式化开发非递归Koch曲线算法  

Formal Development of Non-recursive Algorithm for Koch Curve

作　　者：刘润杰[1] 申金媛[1] 穆维新[1] 

机构地区：[1]郑州大学信息工程学院,郑州450001

出　　处：《计算机科学》2011年第9期126-129,共4页Computer Science

基　　金：河南省教育厅自然科学研究计划项目(2010A510015;2008B120010);江西省高性能计算技术重点实验室开放课题资助

摘　　要：形式化方法是构建可信软件的重要途径。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.

关 键 词：KOCH曲线 形式化方法 非递归 PAR方法 循环不变式 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]