分形理论在通信、现代医学、流体力学、纺织科学、工业设计、文化艺术、计算机科学等学科也得到广泛的应用。形式化方法是一种基于数学方法的规约，技术和验证系统的工具。它不仅使用在系统验证方面，而且在算法的形式开发推导方面也起到重要作用。分形算法在通信领域具有越来越广泛地应用，如保密通信、扩频通信、数据压缩等。但是分形算法的开发很少使用形式化方法来开发，其可靠性和正确性难以保证，从而影响了分形算法在正确性和可靠性要求高的系统中的应用。本文主要工作是研究形式化方法在分形算法上的应用。首先分析分形图形的数学理论，结合PAR方法开发算法程序的步骤，得到一种非递归的分形算法。其次，本文分析了分形图像编码压缩算法，结合PAR方法的规约变换规则，对算法进行形式推导，保证了开发算法的正确性。本文的贡献和主要内容：第一：分析了PAR方法开发算法程序的步骤和规约变换规则，结合了分形理论在开发分形图形时所需求的基本特性（具有自相似性、仿射变换等特性），提出使用PAR方法来开发分形图形生成算法。第二：基于PAR方法形式开发得到的Apla语言描述的分形图形算法和循环不变式。采用Dijkstra算法证明方法验证开发算法的正确性。然后使用PAR开发平台中的Radl-Apla转换器，把Apla程序转换成可以在机器上执行的高级语言程序。最后又对形式开发的非递归程序进行分析。第三：基于分形理论在分形图形编码上的应用研究，使用PAR方法形式开发算法规约的变换规则，形式推导出分形图像编码算法。形式化开发该算法的优点：从形式化的角度分析了复杂算法的结构，使得复杂算法变得简单易懂；在理论上推导分形编码算法的过程。扩展了PAR方法在复杂算法程序开发上的应用。