Formal Development of Non-recursive Algorithm for L-system Based Koch Curve

Formal method is an important approach for construction of the trustworthy software. Koch curve is one of the typical fractals. Employing PAR method and the strategy of developing loop invariant, this paper develops non-recursive algorithmic program of L system based Koch curve and verifies the program formally. This paper aims at non-recursive algorithms directly", "and achieves loop invariant of L system based Koch curve with readable", "efficient and reliable non-recursive algorithm finally. The paper contributes to developing non-recursive algorithm using formal method and new strategy of developing loop invariant.