关键词: 折半划分, 形式化推导, 分划递推, 程序求精

Abstract: Formal derivation is the program development under the theory of program correctness proof, and finally obtains the completely correct algorithm program. Regarding the problem of sequence dimidiate partition, the existing formal derivation method alternates the derivation and proof in the derivation process. The derivation process is cumbersome and most of them cannot directly obtain the executable program. To solve the above problems, this paper proposes a new formal derivation method for the sequence dimidiate partition problem. This method is based on the core idea of partition and recursion, applies the specification transformation technology to transform the problem specification and strictly guarantee its consistency, so that there is no need to proof in the derivation process. Then, the recurrence relations are derived and a highly reliable Apla program is obtained. Finally, the conversion tool is used to automatically generates executable programs. It realizes the complete process of program refinement from the program specification to the specific executable program. By taking two algorithms as examples, the effectiveness and feasibility of the method are verified. It has guided significance for the formal derivation of related problems.

Key words: dimidiate partition, formal derivation, partition and recursion, program refinement