算法的正确性

来自计算思维百科
跳转至: 导航搜索

一个正确的算法是对每一个输入数据产生对应的正确结果并且停止。也就是说一个正确的算法能够解决给定的计算问题。而错误的算法对于某些输入数据要么不会停止,要么在停止前给出的不是预期的正确结果。

错误的算法就一定没有用么?答案是不一定。正确性和效率有的时侯是相互矛盾的,如果一个错误算法的错误率和错误程度可以被控制在一定范围内,而它的效率比保证正确的算法高很多,那么它也可能是有用的。例如,启发式算法和近似算法常用于求解NPC问题,它们往往不能计算出最优结果,但其计算时间通常远快于可计算出最优结果的算法。

算法正确性的重要性

在很多应用领域中,算法的正确性是至关重要的。因为算法或程序的错误而造成重大损失甚至灾难的例子并不鲜见。例如,20世纪60年代初期,由于飞行控制计算机程序中的一个错误,发射到金星的美国太空船水手号不幸失事,损失数百万美元。

设计出算法后,证明该算法对所有可能的合法输入都能计算出正确结果的工作过程称为‘算法确认'(Algorithm Confirmation)算法确认与描述实现这一算法的手段无关,例如可以用不同计算机语言来实现同一算法。用算法语言描述构成的程序在计算机上运行,也应证明该程序是正确的,这一工作称为程序证明'(Software Verification)。

算法确认和程序证明的研究难度非常大,最主要的途径是采用形式化逻辑的方法。其中格里斯(D.Gries)于1980年综合了以谓词演算为基础的证明系统,称之为“程序设计科学”,首次把程序设计从经验和技术升华为科学。中国数学家吴文俊继承和发展了中国古代数学传统的算法化思想,研究几何定理的机器证明,彻底改变了这个领域的面貌,是国际自动推理界的先驱之一。

SPARK语言是程序证明领域的主要研究成果之一。它已经被应用到包括美国国土安全部和洛克希勒.马丁公司等在内的多个软件开发项目中。应该指出的是,本领域还没有很多可以广泛应用的研究成果。也就是说,从理论角度证明算法和程序的正确性在大部分软件系统中是现阶段难以实现的。在这种情况下,往往采用测试的方法验证软件系统的重要性。虽然不能保证100%的正确性,科学高效的测试对于软件正确性的提升裨益良多。