什么样的程序才是正确的？如何来保证程序是正确的？
测试？NO！采用测试方法确实可以发现程序中的错误，但却不能保证和证明程序中没有错误！
先来看一些概念，有关程序功能的精确描述
前置断言：程序执行前的输入应满足的条件，又称为输入断言。
后置断言：程序执行后的输出应满足的条件，又称为输出断言。
程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。
程序设计一般过程：问题 -----> 程序规约 ----->程序
程序规约的分类
非形式化程序规约: 非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。
形式化程序规约: 采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。
衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。
对程序的正确性理解，可以分为两个层次：
从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。
从狭义而言，如果一个程序满足了它的程序规约就是正确的。
程序规约Q{S}R 是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为 “程序S，关于前置断言Q和后置断言R是完全正确的”。
部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。
程序终止：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。
完全正确：程序是部分正确，同时又是终止的
在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。
求数组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])}
求两个非负整数的最大公约数。
[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)}有些程序里面会有循环，这里也需要证明。
循环不变式
初始化：在循环的第一轮迭代前是正确的；
保持：如果在循环的某一次迭代开始之前是正确的，那么在下一次迭代开始之前，也是正确的；
终止：当循环结束，不变式给了我们一个有用的性质。
当头两个性质成立时，就能保证循环不变式在循环的每一轮迭代开始之前，都是正确的，有关循环不变式的第三项可能是最重要的，因为我们是用不变式来证明算法的正确性。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
