三个经典数学问题的形式化开发

Formal Development of Three Classical Mathematics Problems

计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。

Turing Award in computer science prizewinner Knuth says algorithm is the core of computer science.Algorithm design and understanding are important to the development of efficient and correct software.This paper,through the formal PAR derives square number,geometric sum and an polynomials evaluation achieves the three classical mathematical problem,from the problem of exact function to be described starting,uses the PAR method and PAR platform reasoning and transformation rules,after a series of equivalent transformation,gets the correct algorithm program finally.This process reveals three classical mathematical problem subtleties.Facts show that PAR method and platform can play a greater role in the algorithm and program design process.