论文部分内容阅读
The development of algebraic and numerical algo-rithms is a kind of complicated creative work and it is difficult to guarantee the correctness of the algorithms.This paper introduces a systematic and unified formal development method of algebraic and numerical algorithms.The method implements the complete refinement process from abstract specifications to a concrete ex-ecutable program.It uses the core idea of partition and recursion for formal derivation and combines the mathematical induction based on strict mathematical logic with Hoare axiom for correct-ness verification.This development method converts creative work into non-creative work as much as possible while ensuring the correctness of the algorithm,which can not only verify the correctness of the existing algebraic and numerical algorithms but also guide the development of efficient unknown algorithms for such problems.This paper takes the non-recursive implementation of the Extended Euclidean Algorithm and Homer's method as examples.Therefore,the effectiveness and feasibility of this method are further verified.