程序的正确性证明PPT课件.ppt

《程序的正确性证明PPT课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第三章程序的正确性证明主要内容程序的测试Floyd-Hoare规则公理方法Dijkstra最弱前置条件方法程序的正确性所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”一段程序是错误的，是指：（1）程序完成的事情并不是程序员想要完成的事情；（2）程序员想要程序完成的事情，程序并没有完成。一般来说，程序中含有错误是很难避免的。错误可能有：（1）设计时的错误；（2

2、）程序编写时的错误；（3）运行时的错误等。发现错误或尽量减少错误，是程序设计人员的努力方向，更是其职责。如何保证程序的正确性要求1、从编程时就应该尽量地避免和减少错误的发生2、当程序编好后要尽量找出错误，纠正错误避免错误的方法1、程序的结构要简单2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法发现错误的方法1、利用测试工具:跟踪程序的运行，用测试的办法去查找并发现程序错误；2、利用程序的验证系统：证明程序的正确性。程序测试：给程序一组或几组初始值进行试运行，将运行的结果与实现已知的结果比较，若两则相同，则认

3、为程序是正确的，若两则不同，则说明程序有错误。一、程序测试软件测试的目的基于不同的立场，存在着两种完全不同的测试目的。从用户的角度出发，普遍希望通过软件测试暴露软件中隐藏的错误和缺陷，以考虑是否可接受该产品。从软件开发者的角度出发，则希望测试成为表明软件产品中不存在错误的过程，验证该软件已正确地实现了用户的要求，确立人们对软件质量的信心。程序测试1983年IEEE提出的软件工程术语中给软件测试下的定义是：“使用人工或者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别

4、。”测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试

5、用例，出错统计和最终分析报告，为维护提供方便。程序测试实质上只是一种抽样检查测试过程：选取测试数据→执行程序→输入测试数据→记录执行结果→手工核对结果因此，测试只是一种查错的手段，它可以帮助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的程序测试的过程…软件测试方法软件测试的方法和技术是多种多样的。对于软件测试技术，根据不同角度，可以将测试方法分为不同种类。（1）从是否需要执行被测软件的角度，可以分为静态测试和动态测试；（2）从测试是否针对系统内部结构和具体实现算法的角度，可以分为白盒测试和黑

6、盒测试；（3）从实际测试的前后过程来看，软件测试是由一系列的不同测试组成，这些步骤可以分为：单元测试、组装测试（集成测试）、确认测试和系统测试。两种重要的软件测试方法黑盒测试这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。黑盒测试又叫做功能测试或数据驱动测试。白盒测试此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。通过在不同点检查程序的状态，

7、确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误:是否有不正确或遗漏了的功能?在接口上，输入能否正确地接受?能否输出正确的结果?是否有数据结构错误或外部信息(例如数据文件)访问错误?性能上是否能够满足要求?是否有初始化或终止性错误?用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。但这是不可能的。假设一个程序P有输入量X和Y及输出量Z。在字长为32位的计算机上运行。若X、Y取

8、整数，按黑盒方法进行穷举测试：可能采用的测试数据组：232×232＝264如果测试一组数据需要1毫秒，一年工作365×24小时，完成所有测试需5亿年。软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：对程序模块的所有独立的执行路径至少测试一次；对所有的逻辑判定，取“真”与取“假”的两种情况都至少