第六课 程序正确性证明
第六课 程序正确性证明
本章主要研究内容 基本概念 程序测试的基本方法 部分正确性证明方法 终止性证明方法
本章主要研究内容 ◼ 基本概念 ◼ 程序测试的基本方法 ◼ 部分正确性证明方法 ◼ 终止性证明方法
基本概念一程序正确性的定义 段程序是正确的,是指这段程序能正确无误地完成程 序设计时所期望的功能。或者说:对任何一组允许的输入信 息,程序执行后能得到一组和这组输入信息相对应的正确的 输出信息。程序的正确性是衡量一个程序是否优秀的最基本 条件。 段程序是错误的,是指(1)程序完成的事情并不是程序 员想要完成的事情;(2)程序员想要程序完成的事情,程 序并没有完成。 一般来说,程序中含有错误是很难避免的。错误可能有(1 设计时的错误;(2)程序编写时的错误;(2)运行时的错 误等。 发现错误或尽量减少错误,是程序设计人员的努力方向,更 是其职责
基本概念-程序正确性的定义 ◼ 一段程序是正确的,是指这段程序能正确无误地完成程 序设计时所期望的功能。或者说:对任何一组允许的输入信 息,程序执行后能得到一组和这组输入信息相对应的正确的 输出信息。程序的正确性是衡量一个程序是否优秀的最基本 条件。 ◼ 一段程序是错误的,是指(1)程序完成的事情并不是程序 员想要完成的事情;(2)程序员想要程序完成的事情,程 序并没有完成。 ◼ 一般来说,程序中含有错误是很难避免的。错误可能有(1) 设计时的错误;(2)程序编写时的错误;(2)运行时的错 误等。 ◼ 发现错误或尽量减少错误,是程序设计人员的努力方向,更 是其职责
基本概念一程序测试 何发现错误或尽量减少错误? (1)设计程序时尽可能使用结构化程序设计方法,使程序 设计过程规范化和标准化; (2)程序调试或运行时采用测试的方法去跟踪程序的运行, 从而发现与改正错误; (3)利用程序正确性证明的方法检验程序是否正确 ■程序测试:给程序一组或几组初始值进行试运行,将运行的 结果与实现已知的结果比较,若两则相同,则认为程序是正 确的,若两则不同,则说明程序有错误
基本概念-程序测试 ◼ 如何发现错误或尽量减少错误? ◼ (1)设计程序时尽可能使用结构化程序设计方法,使程序 设计过程规范化和标准化; ◼ (2)程序调试或运行时采用测试的方法去跟踪程序的运行, 从而发现与改正错误; ◼ (3)利用程序正确性证明的方法检验程序是否正确。 ◼ 程序测试:给程序一组或几组初始值进行试运行,将运行的 结果与实现已知的结果比较,若两则相同,则认为程序是正 确的,若两则不同,则说明程序有错误
程序测试 一个软件的开发过程要经过程序设计, 设计,编写,测试与证明等一系列过程 后,才能投入使用。已编写好的软件是 否有错误是用户极其关心的问题
程序测试 ◼ 一个软件的开发过程要经过程序设计, 设计,编写,测试与证明等一系列过程 后,才能投入使用。已编写好的软件是 否有错误是用户极其关心的问题