循环不变式

程序的正确性

• 程序的正确性

  • 程序能否按照预定的要求完成预定的功能，且打到预定的效果。
  • 对于程序的任何一组允许的==输入数据==，程序执行后都能得到一组与之相对应的正确的==输出数据==。

• 程序测试

  • 不可能对所有可能的输入去测试其输出是否正确。

  • 测试只能证明程序有错误，不能证明程序无错误。

• 程序正确性证明

  • 直接对源程序证明其正确性的过程，是一种逻辑证明方法。

确定循环过程是正确的

• 找到循环不变式（Loop Invariant）
  • 在循环体中选取一个点， 在该点处建立一个断言（逻辑表达式）
  • 使得每次循环执行到该点时，这个逻辑表达式在循环体中总为“真”。
  • 不依赖于前面所执行过的循环次数以及变化量的变化。
  • 表示的是一种在循环过程进行时保持不变的性质。

计算自然数的乘法$a * b$

• $a+a+a+...$ 用加法实现乘法

st=>start: 开始
e=>end: 结束
in=>inputoutput: 输入a和b
op1=>operation: i = 0,sum = 0
cond=>condition: i < b ?
op2=>operation: sum = sum + a
op3=>operation: i = i + 1
out=>inputoutput: 输出sum
st->in->op1->cond
cond(yes)->op2->op3(left)->cond
cond(no)->out->e

每次加一个a，循环b次

随着i值增加， sum逐渐趋近于所求的值

---

$sum = a * i$	i
$sum = a * 1$	1
$sum = a * 1$	2
$sum = a * 3$	3
	…
$sum = a * b$	b

循环不变式P

• $$sum + (b-i) * a = b * a$$
• $i = b$ 时循环结束, sum为所求值
• 循环条件为: $i<b$

采用迭代法计算两个正整数的商和余数

• 设被除数为x,除数为y,商为q,余数为r
  • 根据商和余数的关系: $x = q * y + r$
  • 令余数r的初值为被除数x
  • 不断从r中减去除数y,知道无法从r中减去y时为止
• 循环不变式P: $x = q * y + r$
  • r < y时, 循环结束,q和r即为所求
  • 循环条件为: r>=y

st=>start: 开始
e=>end: 结束
in=>inputoutput: 输入x和y
op1=>operation: q = 0,r = x
cond=>condition: r < y ?
op2=>operation: r = r - y
op3=>operation: q = q + 1
out=>inputoutput: 输出q和r
st->in->op1->cond
cond(yes)->op2->op3(left)->cond
cond(no)->out->e

找到合适的循环不变式只能庁程序的部分正确性,要想验证程序的完全正确行,需证明:1.循环体时可终止的;2.执行程序循环体时必须改变一个或多个变量的值,以保证在经过有限次重复后循环的控制条件不在满足.

循环的可终止性

每次执行$i = i + 1$后, 都使得i增大,知道i值大到不再满足$i <= b$时,循环结束.

st=>start: 开始
e=>end: 结束
in=>inputoutput: 输入a和b
op1=>operation: i = 1,sum = 0
cond=>condition: i <= b ?
op2=>operation: sum = sum + a
op3=>operation: i = i + 1
out=>inputoutput: 输出sum
st->in->op1->cond
cond(yes)->op2->op3(left)->cond
cond(no)->out->e

每次执行 $r = r - y$ 后,都使得r值减小,知道r值小到不再满足 $r >=y$时,循环结束,但不能用q作为循环控制变量.