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.

Key words: Koch curve, Formal method, Non-recursive, PAR method, Loop invariant