计算机问题求解 – 论题2-1 - 算法的正确性 2018年3月7日.

Presentation on theme: "计算机问题求解 – 论题2-1 - 算法的正确性 2018年3月7日."— Presentation transcript:

1 计算机问题求解 – 论题 算法的正确性 2018年3月7日

2 这段话和我们今天的主题什么关系？ 算法问题的完整表达； 解这个问题的算法正确性表现为算法结束时这个relationship必须保持为true

3 Reverse a string:

4 Input: a string of symbol S; Output: the reverse image of S. 算法： 如右图
问题: Input: a string of symbol S; Output: the reverse image of S. 算法： 如右图 For( i=0 to n,i++) sum=sum+i;

5 问题1: 人们似乎对于计算机 “犯错”比对于人犯错更 加苛刻,这是为什么呢?
do precisely what we intend them to do

6 几种不同的错误 “语言错” “语义错” 解题逻辑错误 逻辑错误不常见，但这个是真的“伤脑筋”！ 很容易被语言处理软件发现，甚至自动纠正。
合格的程序员很少会犯这类错误。 解题逻辑错误 “粗心”造成的错误。 常见(相对来说) “真正的”逻辑错误。 举例，判断； 语言错：不符合语法； 语义错：算法正确，但是翻译成程序时出错，使得程序的能力和算法的能力不一致：循环控制出错、键盘输入错误； 逻辑错误：指算法错误，比如统计员工工资。问题理解出错，计划出错等。 逻辑错误不常见，但这个是真的“伤脑筋”！

7 问题2： 书上的对文本中出现“money”一词的句子计数的 例子出现了什么样的错误，你能说出它的性质吗？ 问题：出现money的句子有多少？

8 Test and debugging A designer might try out an algorithm on several typical and atypical inputs and do not find the error. In fact, a programmer will normally test a program on numerous inputs, sometimes called test sets, and will gradually rid it of its language errors and most of its logical errors. Most algorithmic problems have infinite sets of legal inputs, and hence infinitely many candidate test sets, each of which has the potential of exposing a new error.

9 Debugging 的局限性 我们能够用形式系统为Dijkstra的话证实吗？
As someone once put it, testing and debugging can not be used to demonstrate the absence of errors in software, only their presence. “someone” believed to be Dijkstra: Program testing can be used to show the presence of bugs, but never to show their absence! Algorithmic errors can go undetected for ages. 我们能够用形式系统为Dijkstra的话证实吗？

10 关于debugging的思考 为什么我们可以： The process of repeatedly executing an algorithm, or running a program, with the intention of finding and eliminating errors is called debugging？ 运行环境的封闭性。开放的并发环境，debug将异常困难。

11 如何避免不正确的Infinite loop出现？
Infinite computation 为什么infinite computation 有时也被称为 infinite loop? Infinite loop有什么作用？ 循环控制必须慎重选择：有界（计数）循环 VS 无界（判定）循环！ 17.6？ 最好不要用“相等”进行循环出口的判断！ 如何避免不正确的Infinite loop出现？

12 部分和完全正确性 区别在于是否考察算法是否会终止，共同点在于：relationship得到了保证

13 当我们完成了某个算法的正确性证明，我们test的，debug的是什么？
算法正确性证明： 自动验证： some sort of super-algorithm that would accept as inputs a description of an algorithmic problem P and an algorithm A that is proposed as a solution, and would determine if indeed A solves P. 人工证明： Can we ourselves prove our algorithms to be correct? Is there any way in which we can use formal, mathematical techniques to realize this objective? 当我们完成了某个算法的正确性证明，我们test的，debug的是什么？

14 如何利用什么数学技术来证明算法的正确性？
“部分正确性”： We do not care whether execution ever reaches the endpoint, but that if it does we will not be in a situation where the outputs differ from the expected ones. we wish to capture the behavior of the algorithm by making careful statements about what it is doing at certain points. we thus attach intermediate assertions to various checkpoints in the algorithm’s text. Accordingly, we wish to capture the behavior of the algorithm by making careful statements about what it is doing at certain points

15 什么是assertion？ 一个可以被证明是否为真的命题！

16 我们可以在算法的任意位置，设置assertion
这个“位置”就是check point

17 如何理解以下文字？ Attaching an assertion to a checkpoint means that we believe that whenever execution reaches the point in question, in any execution of the algorithm on any legal input, the assertion will be true.

18 那么是否每个算法都只要这两个断言即可呢？
我们用assertion可以做什么？ Assertion1: S is a symbol string 可以用来判断任意输入的合法性 Assertion3: Y = reverse(S) 如果每个合法的输入，算法都能 运行到这一点并且断言3都为真， 算法的部分正确性就能得到证明！ 那么是否每个算法都只要这两个断言即可呢？ 因为我们要面对“任意的输入”，我们很难直接面对最后的断言，进行证明。我们必须、几乎要考察每一个算法步骤，看是否形成一个“真断言” 链，看这个链在reach终止点时，能否“推理”出终止点断言的truth。

19 Reverse a string: 复习这个算法

20 其实，循环部分的正确性证明是部分正确性证明的关键所在，因此，在多数情况下，不包含递归的算法的部分正确性证明，往往忽略非循环部分的断言设置和证明
真断言链：

21 什么是证明了这个算法的部分正确？ 证明就是断言的序列 (断言必须为真) 断言序列中断言是否为真，需要利用算法步骤的内在含义进行证明：
有些checkpoint不断被reach，其断言也必须不断被证真：

22 问题: 这些intermediate assertions 为什么被 称为“invariants”? 什么又叫循环不变式？
points that are reached many times within a single execution. they remain true no matter how often they are reached.

23 Then: 要证明一个算法的部分正确性： 在哪里设置checkpoint？ 什么样的“局部特性”用断言形式描述？ proceeding locally from checkpoint to checkpoint does not bring about any violations of the invariance properties 循环体内的循环起始点，通常需要设置checkpoint，定义循环不变式

24 问题： 你能指出循环不变式是什么吗？ Ck = A  Dk //这个过程计算A的平方 subroutine square of A:
set C to 0; set D to 0; while (D≠A) do set C to C +A; set D to D +1; (4) return C . //这个过程计算A的平方 问题： 你能指出循环不变式是什么吗？ Ck = A  Dk

25 收敛性：total正确性的证明方法 There must be a bound!
showing that something good eventually happens (not that bad things do not); namely, that the algorithm indeed reaches its endpoint and terminates successfully. find some quantity and show that it converges: quantity keeps decreasing as execution proceeds from one checkpoint to another, but that it cannot decrease forever: there is some bound below which it can never go There must be a bound! 写循环，必须清醒地认识到这一点！

26 “部分”与“完全”正确性 问题： 你能否用这个例子解释 Partial 和 Total正确性？ Euclid algorithm
input: nonnegative integer m,n output: gcd(m,n) procedure Euclid(int m,n) if n=0 then return m else return Euclid(n, m mod n) if d is the GCD of m and n, it must be the GCD of n and (m mod n) 1 问题： 你能否用这个例子解释 Partial 和 Total正确性？ (m mod n) is always less than n, so, the algorithm must terminate 2

27 但是，针对递归算法：

28 我们有类似的思考 Our expectation of Move:

29 Then: 问题：这种方法和我们用循环不变量的保持证明循环的正确性有何差异？
我们用数学归纳法证明 the expectation holds for every N! 问题：这种方法和我们用循环不变量的保持证明循环的正确性有何差异？

30 HOMEWORK DH： 5.6；5.9；5.10；5.12； 证明欧几里得算法的部分正确性