Chinese Journal of Computers   Full Text
Title	PAR-Based Formal Development of Algorithms
Authors	SHI Hai-He1),2),3) XUE Jin-Yun1),3)
Address	1)(National Key Laboratory for Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190) 2)(Provincial Key Laboratory for High-Performance Computing Technology, Jiangxi Normal University, Nanchang 330022) 3)(Graduate University of Chinese Academy of Sciences, Beijing 100049)
Year	2009
Issue	No.5(982—991)
Abstract &   Background	Abstract Formal method is an important approach for construction of the trustworthy software. Based on the analysis of algorithmic problems and the features of formal method PAR, the laws of problem partition and recurrence relation construction are described. From a class of problem formal functional specification, the problem partition and the specification transformation can be done mechanically, the ideas behind algorithmic solutions can be discovered naturally, and further the resultant algorithmic programs can be produced automatically by means of tools. The research result makes as much creative work as possible converted into routine work, and the difficulty of formal algorithmic problem solving is reduced substantially, thus enables the improvement of reliability and productivity of algorithmic programs. Keywords algorithms; formal method; PAR; specification; trustworthy software Background The work is supported by the National Natural Science Foundation of China (Nos.60573080, 60773054), the International Science and Technology Cooperative Program of China (No.2008DFA11940), and the Provincial Natural Science Foundation of Jiangxi (No.2008GQS0056). Recently trustworthy software has been proposed and advocated by many countries and many academic communities. Formal method is an important approach for construction of the trustworthy software, and many researches are in the ascendant. Some of them are built upon the Gries’ vision of developing a program and its proof of correctness hand in hand, where the loop invariant must be developed beforehand. Some of them apply program transformation technique to the development of programs, where the start point of transformation is an initial inefficient program and aims to transform it into equivalent, more efficient one. Some other researches try to implement automatic development from problem specification to executable code through specification refinement, and provide large reusable libraries for construction and refinement of specification. Yet, due to the creativity involved, especially because of the difficulty of developing crucial loop invariant, algorithm formal method still remains to be one of the field’s most challenging problems. Its use so far within the software development community has not been commensurate with its potential. Therefore, it is necessary to explore the laws or essentials behind algorithm design. Based on a unified and practical formal method PAR that is the outcome of the authors’ research on several National Natural Science Foundation projects of China, and putting the efficiency of resultant algorithms first, the paper proposes the problem partition rules and recurrence construction strategies. With the rules and strategies, one of a class of problems is partitioned into the sub-problems, recurrences of problem solving sequence are constructed from problem formal functional specification, and the resultant algorithmic programs can be produced automatically by means of tools. Practice shows us that with the rules and strategies not only a known ingenious algorithm but also a new one for a given problem may be derived mechanically. It makes as much creative work as possible converted into routine work, thus minimizes algorithm designers’ efforts and enables the improvement of productivity and reliability of algorithmic programs.