第六课 程序的正确性证明.ppt

第六课程序正确性证明
本章主要研究内容
基本概念
程序测试的基本方法
部分正确性证明方法
终止性证明方法
基本概念-程序正确性的定义
一段程序是正确的,是指这段程序能正确无误地完成程序设计时所期望的功能。或者说:对任何一组允许的输入信息,程序执行后能得到一组和这组输入信息相对应的正确的输出信息。程序的正确性是衡量一个程序是否优秀的最基本条件。
一段程序是错误的,是指(1)程序完成的事情并不是程序员想要完成的事情;(2)程序员想要程序完成的事情,程序并没有完成。
一般来说,程序中含有错误是很难避免的。错误可能有(1)设计时的错误;(2)程序编写时的错误;(2)运行时的错误等。
发现错误或尽量减少错误,是程序设计人员的努力方向,更是其职责。
基本概念-程序测试
如何发现错误或尽量减少错误?
(1)设计程序时尽可能使用结构化程序设计方法,使程序设计过程规范化和标准化;
(2)程序调试或运行时采用测试的方法去跟踪程序的运行,从而发现与改正错误;
(3)利用程序正确性证明的方法检验程序是否正确。
程序测试:给程序一组或几组初始值进行试运行,将运行的结果与实现已知的结果比较,若两则相同,则认为程序是正确的,若两则不同,则说明程序有错误。
程序测试
一个软件的开发过程要经过程序设计,设计,编写,测试与证明等一系列过程后,才能投入使用。已编写好的软件是否有错误是用户极其关心的问题。
程序测试
程序测试的目的是为了发现程序的错误
程序测试的方法是按习惯挑选各种数据,设计测试用例程序
程序测试
我们测试的程序一般有两种情况:
知道程序的输入和输出功能,而不知道程序的具体结构(常称为黑盒子方法)
已知程序内部结构和流向,测试的用例是根据程序内部逻辑来设计的(白盒子方法)
黑盒子测试方法
在VAX计算机上(字长32位),输入X,Y整数,运行程序后输出Z,则输入数据可能值有2的64次方种可能。
如果执行程序一次要1毫秒,那么对所有数据进行测试需要5亿年
白盒子测试方法(图例)
白盒子测试方法(续)
一程序流程如前图所示。其中从a到b有5种路径,再外套循环20次,这样一个小程序的路径测试就有5的20次方种。
如果程序执行一次从a到b平均花1分钟,整个路径需要运行2亿年才能走遍。