QCP Tutorials 规约标注入门

如果程序比较简单，并且待验证的性质也比较简单，那么QCP往往就可以自动完成验证。T1-1中列举的add等例子都属于这一类。然而，当程序复杂一些，哪怕只是包含循环结构时，QCP就无法自动完成验证。用户可以使用断言标注辅助QCP完成验证。在所有断言标注中，最主要的就是循环不变量标注。

例子：简单循环

下面程序通过一个C语言的for循环实现了加法的功能。

int slow_add(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  int i;
  /*@ Inv Assert
        y == y@pre + i && x == x@pre &&
        0 <= i && i <= x@pre &&
        0 <= x@pre && x@pre <= 100 && 
        0 <= y@pre && y@pre <= 100
   */
  for (i = 0; i < x; ++ i) {
    y ++;
  }
  return y;
}

其中以Inv Assert开头的断言标注就是循环不变量，它表示每次程序检查for循环条件i < x的时候，程序变量都符合这个条件。如下图所示。

这个断言中的x@pre和y@pre表示两个参数传入该C函数时候的值，换言之，这个断言说的是：y的当前值是y的初始值加上i，并且i在0到x的范围之内。基于这个循环不变量，QCP只需要检查以下3个条件就可以确认该C函数确实实现了加法：

• 初始化i = 0之后，程序状态满足不变量y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre（关于x@pre与y@pre本身的性质这里不再重复，下同）；
• 如果程序状态满足不变量y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre，并且会进入循环体（因此i < x为真），那么执行循环体y ++以及++ i之后，循环不变量依然成立；
• 如果程序状态满足不变量y == y@pre + i && x == x@pre && 0 <= i && i <= x@pre，并且此时不会再进入循环体（因此i < x为假），那么执行循环后的return y语句后能够保证Ensure条件__return == x@pre + y@pre成立。

由于已知x@pre与y@pre都在0到100的范围内，不难发现上述三条性质确实成立，QCP也能自动验证这一点。