软件功能验证与优化的研究

摘要

按照通常的观点,软件由程序和文档两部分构成,文档的检测涉及太多的非技术的因素,而目前在软件测试性计算的文献中多把程序测试性和软件测试性当作同一概念,借用此观点,这里所讨论的软件的功能验证,也就是程序的功能验证.程序的正确性验证包括两个方面的问题:一是在准确给出程序的功能的情况下,对给出的功能一一验证;二是在没有准确给出程序功能的情况下,看给定的程序可以完成哪些功能.前者是功能验证,后者是功能检测.而本文所讨论的软件功能验证就可以归结为程序的功能验证,从而也就归属于程序的正确性验证问题.对程序的正确性验证问题,现在已经做了大量的工作,但大多数都是用逻辑的方法来研究的,这里,想简单介绍用逻辑方法验证程序的正确性,并提出另一种思路:用代数的方法来解决此问题,并从代数的角度来说明软件的优化问题.