| 在程序中的特定部位插入某些用以判断变量特性的语句，使得程序执行中这些语句得以证实，从而使程序的运行特性得到证实。我们把插入的这些语句称为断言（assertions）。这一作法是程序正确性证明的基本步骤，尽管算不上严格的证明，但方法本身仍然是很实用的。下面以求两个非负数NUM和DEN之商的Wensley迭代算法为例，对断言语句的作用作一简要说明。
|
|
|
| 假定两个非负数中，NUM小于M（即所得之商小于1），算法中只用到加、减及除2的运算。该迭代算法的程序如下图所示。
|
|
|
|
|
|
|
| 从程序中可以看出，在每次迭代中由分母得到的变量B以及权增量W都要缩小一半，而且变量A随着迭代次数的增加将接近分子。这些粗略的观察和分析可以用以下4个断言语句表达，在每次迭代开始时4个断言必定为真：
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 假定我们所用的编译系统能够处理表达式形式的断言语句，插入断言以后的程序如下图所示。其中带有标记@的语句是断言语句。新增加的变量K只是在计算第①断言时用到。
|
|
|
|
|
|
|
|
|
|
|
|
|
| ③将W的值代入DEN * W/2，则得B的初值：B＝DEN/2。
|
|
|
|
|
| 以上说明了这些断言在初始状态下为真。如果继续迭代，要证明断言为真，就必须证明无论if-then结构中执行什么路径这些断言都为真。我们先来考虑在初始测试中NUM-A-B≥0为假，即检验失败，然后给出程序向量的新值（A′，B′，W′，Q′和K′），我们有：
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| ③ B*=B/2=DEN * W/4=DEN* W*/2
|
|
|
| ④把A和B代入（NUM-A-B<0），得到NUM-DEN * Q-DEN * W/2<0，对此关系式两端除以DEN，并加Q，得到，由于Q′＝Q, W′＝W/2，我们有NUM/DEN-W**，且Q≤NUM/DEN。
|
|
|
| 如果if-then检验成立，再来看4个断言。使用A″，B″，W″，Q″和K″作为新的程序向量，我们有：
|
|
|
|
|
| ②A"=DEN * Q+DEN * W/2=DEN *（Q+W/2）=DEN * Q"
|
|
|
| ③ B″=B/2=DEN * W/4=DEN * W″/2
|
|
|
| ④代入（NUM-A-B ≥ 0），并作同前的变换，得到NUM/DEN - W″/2
|
|
|
| 总之，无论执行哪一路径，在每一迭代的开始，4个断言均为真。尽管并未考虑输出断言，但是我们知道，第④断言成立，由于W
|
|
|
