华中科技大学：《程序设计方法学》第六课 程序的正确性证明

第六课 程序正确性证明

第六课 程序正确性证明

本章主要研究内容 基本概念 程序测试的基本方法 部分正确性证明方法 终止性证明方法

本章主要研究内容 ◼ 基本概念 ◼ 程序测试的基本方法 ◼ 部分正确性证明方法 ◼ 终止性证明方法

基本概念一程序正确性的定义 段程序是正确的,是指这段程序能正确无误地完成程 序设计时所期望的功能。或者说:对任何一组允许的输入信 息,程序执行后能得到一组和这组输入信息相对应的正确的 输出信息。程序的正确性是衡量一个程序是否优秀的最基本 条件。 段程序是错误的,是指(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亿年才能走遍