T3-4 - 符号执行遇到断言标注的情况

QCP工具允许用户在程序语句间添加断言标注辅助验证的完成。前面曾经提到的循环不变量就是一种这样的断言标注。当QCP符号执行器遇到断言标注时，就会检查先前由符号执行得到的最强后条件是否可以推出用户手动输入的断言。以前面曾经介绍过的swap函数为例。

void swap(int * px, int * py)
/*@ With x y
    Require store_int(px, x) * store_int(py, y)
    Ensure store_int(px, y) * store_int(py, x) */
{
  int t;
  t = * px;
  * px = * py;
  * py = t;
}

第一条赋值语句执行后，程序状态满足下面断言（这也是QCP符号执行器会得到的最强后条件）：

store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)

其中，px_37和py_40表示px@pre和py@pre这两个初始值。当然，我们看了后续程序，我们知道此时* px存储的值是没有用的。下面我们就在这个程序点上断言了这个弱一些的性质。

void swap(int * px, int * py)
/*@ With x y
    Require store_int(px, x) * store_int(py, y)
    Ensure store_int(px, y) * store_int(py, x) */
{
  int t;
  t = * px;
  /*@ Assert
        store_int(&t, x) *
        store_ptr(&px, px@pre) *
        store_ptr(&py, py@pre) *
        has_int_permission(px@pre) *
        store(py@pre, y) */
  * px = * py;
  * py = t;
}

添加这条断言就表示“程序执行到此处时程序状态必定满足此性质”，并且后续程序语句的正确性也仅仅由此性质保障。换言之，哪怕我们实际可以论证程序执行到此处时满足更强的性质，后续程序语言的验证也无需用到更强的性质。因此，如果QCP在验证过程中遇到这样带标注的程序，就会生成一条下面这样的验证条件（verification condition, VC，需要验证|--左边的断言能推出|--右边的断言），并且基于用户给出的断言进行后续的符号执行。

store_int(&t, x) *
store_ptr(&px, px@pre) *
store_ptr(&py, py@pre) *
store_int(px@pre, x) *
store_int(py@pre, y)
|-- store_int(&t, x) *
    store_ptr(&px, px@pre) *
    store_ptr(&py, py@pre) *
    has_int_permission(px@pre) *
    store_int(py@pre, y)

下面两图中可以看到符号执行该断言前后的对比。符号执行该断言之后，Normal断言列表中显示了断言标注中引入的has_permission谓词。