A Mechanical Approach for Deriving Algorithmic Programs

Formal algorithm derivation is valuable in ensuring resultant algorithm correctness, revealing ideas behind algorithm, and studying automatic algorithm design. An approach called mechanical partition-and-recur (MPAR for short) for deriving algorithmic program is presented. It is built on top of formal method PAR, and provides a series of strategies for mechanical algorithm derivation. Using MPAR, a given problem is partitioned into sub-problems mechanically, according to which the problem specification is transformed to seek the relation between the solutions of original problem and its sub-problems, and then the executable language program is produced automatically. MPAR makes as much work as possible be shifted from the algorithm designers, and thus enables the improvement of productivity and reliability of software.