Abstract: Designing algorithm is a creative activity. The traditional design and description methods are difficult to ensure the correctness of algorithm. By defining algorithm description language Radl with mathematical referential transparency in the PAR method, the algorithm described by recursive relation can be obtained from deriving problem specification formally. The core of the algorithm is the recursive relation group, and therefore, it is easy to deduce and prove Radl algorithm formally. By deeply analyzing Radl language and Radl algorithm characteristics, the essential relationship between the Radl algorithm and abstract sequential program Apla is revealed, and Apla program generation rules based on Radl grammar productions are defined. Then Apla program automatic generation system is achieved and the systems reliability is studied. Finally the core algorithm of the system is verified formally. The algorithm developed by PAR method is correct, and the generation system which is proved formally can be assured reliably. So the high reliability of algorithm is ensured, and the automation development tools improve the development efficiency of program.