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