| Fractal theory is widely used in many subjects, such as hydromechanics,textile science, industrial design, culture and art, and computer science. Formalmethod, is a specification that based on mathematical methods, as a tool oftechnique and testing system, not only applies in the system testing field, butalso plays an important role in the development of mathematical methodsalgorithm. At the same time, fractal algorithm has found an increasingly wideutilization in communication field, such as securing communication, spreadspectrum communication and data compression. However, formal method isseldom used in developing fractal algorithm. Thus, it’s not easy to secure thevalidity that impact the application of fractal algorithm in the system.The main content of this paper is to research the application of formalmethod in fractal theory. The first step, by combining with developingalgorithmic routine of PAR method, is to analyze the mathematical theory offractal image, and get an unified non-recursive fractal algorithm, which isfeatured with legibility and high reliability. In the second place, the paper alsoanalyse the fractal image coding compression algorithm, according to combinedwith the changing rules of specification of PAR method, and make a formdeduction on algorithm so that secure the reliability of developing algorithm.The main contribution and contents of this paper is:First, by combining with the basic characters (such as self-similarity, affinetransformation) that needed when fractal algorithm is used to develop fractalimage, the paper analyzes the program steps and transformation rule of PARmethod/platform in developing algorithm.Second, based on PAR method formal development, the paper presentsfractal image algorithm that is described by Apla language and loop invariant.Dijkstra method is used to verify the reliability of developing algorithm. Andthen, Radl-Apla transformation tool of PAR developing platform, is applied to transform Apla program into advanced language program that can be performedon machines. At last, the paper makes more researches on non-recursiveprogram of formal development.Third, based on the application researches of fractal theory in fractal imagecoding, the transformation rule of PAR method formal development algorithmdeducted fractal image coding algorithm. The advantages are following: thepaper analyzes the structure of complex algorithm from formal perspective,which made complex algorithm become easier and understandable.To deducethe process of fractal coding algorithm in theory. Meanwhile, it also broadensthe application of PAR method in complex algorithm program. |