文档介绍：第三课 程序设计方法学基本理论 ——程序正确性证明
什么样的程序才是正确的?
如何来保证程序是正确的?
程序正确性概述
关于程序正确性的认识
根据问题的特性和软件所要实现的功能,选择一些具有代表性的数据,设计测试用例。通过用例程序执行,去发现被测试程序的错误。
什么样的程序才是正确的?
“测试”或“调试”方法
采用“测试”方法可以发现程序中的错误,但却不能证明程序中没有错误!
因此,为保证程序的正确性,必须从理论上研究有关“程序正确性证明”的方法。
程序正确性证明发展历程
20世纪50年代 Turing开始研究
1967年,Floyd和Naur提出不变式断言法
1969年,Hoare提出公理化方法
1975年,Dijkstra提出最弱前置谓词和程序推导方法,解决了断言构造难的问题,可从程序规约推导出正确程序,使正确性证明变得实用。
程序正确性理论是十分活跃的课题,不仅可
以证明顺序程序的正确性,而且还可以证明非确
定性程序,以及并行程序的正确性。
程序正确性理论
程序设计的一般过程
程序正确性理论
程序功能的精确描述
1、程序规约:对程序所实现功能的精确描述,
由程序的前置断言和后置断言两部分组成。
2、前置断言:程序执行前的输入应满足的条件,
又称为输入断言。
3、后置断言:程序执行后的输出应满足的条件,
又称为输出断言。
程序设计过程:问题程序规约程序
程序规约的基本分类
非形式化程序规约
非形式化程序规约采用自然语言描述程序功能,简单、方便,但存在二义性,因此,不利于程序的正确性证明。
形式化程序规约
采用数学化的语言描述程序功能,描述精确,无二义性,便于程序的正确性证明。
程序规约的实例(1/2)
在书写程序规约时,使用Q表示前置断言,R表示后置断言,S表示问题求解的实现程序。在前置断言Q之前,还必须给出Q和R中所出现的标识符的必要说明。
例1:求数组b[0 : n-1]中所有元素的最大值。
[in n:integer; in b[0:n-1]:array of integer; out y:integer]
Q: {n ≥ 1}
S
R:{y = MAX(i: 0 ≤ i < n; b[i])}
例2:求两个非负整数的最大公约数。
[in a,b :integer; out y:integer]
Q: {a ≥ 0 ∧ b ≥ 0}
S
R:{y = MAX(i: 1 ≤ i ≤min(a,b) ∧
(a mod i = 0) ∧(b mod i = 0): i)}
程序规约的实例(2/2)
程序正确性定义(1/3)
衡量一个程序的正确性,主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能,则称它为正确的,否则是不正确的。
程序设计过程:问题程序规约程序
对程序的正确性理解,可以分为两个层次:
从广义来说,一个程序的正确性取决于该程序满足问题实际需求的程度。
从狭义而言,如果一个程序满足了它的程序规约就是正确的。