序列折半划分问题的形式化推导

形式化推导是在程序正确性证明理论下所进行的程序开发，最终得到完全正确的算法程序。针对序列折半划分问题，现有的形式化推导方法将推导与证明交替进行，推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题，提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想，应用规约变换技术对问题规约进行变换并严格保证一致性，使得在推导过程中无需交替证明，进而导出递推关系式并得到高可靠性抽象算法程序Apla，最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例，验证了该方法的有效性和可行性，对相关问题的形式化推导具有指导意义。

Formal derivation of the sequence dimidiate partition problem

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.