QCP Tutorials 内存与断言

C语言程序的一大特点是它可以直接通过内存地址对内存进行读写。例如，下面C程序交换了两个地址上的值。

void swap(int * px, int * py)
{
  int t;
  t = * px;
  * px = * py;
  * py = t;
}

QCP要求在表述内存操作有关的规约时要严格区分内存地址相同与内存地址不相同的情况。这里我们仅仅考虑比较常见的px与py为不同地址的情况，换言之它们所指向的内存空间互不相交。这样，我们就可以说：对于任意的数值x和y，如果初始时x存储在地址px上而y存储在地址py上，那么执行swap后，y存储在地址px上而x存储在地址py上。在QCP中，这一规约可以写成如下形式：

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;
}

下面逐一介绍这一规约中的语法元素。

With语句

规约中With x y表示的是“对于任意x与y”以下规约成立。值得一提的是，这里的x与y不是程序变量，它们是逻辑变量，只是用于辅助写出断言或者规约。

store_int等谓词

store_int(px, x)表示在拥有px地址所指向的内存空间，并且地址px上的存储内容是初始化过的，它存储了一个有符号32位整数值x。这里由于px是int *类型的C语言变量，所以QCP能推断出其指向的内存空间一般是一块存储存储有符号32位整数类型的内存空间，所以在写断言时也可以不指明类型，只写store(px, x)。有些时候可能QCP无从完成这样的自动推导，或者我们想要在断言中更明确地说明相关类型，那就可以像上面例子中那样写作store_int(px, x)或者store(px, int, x)。另外，如果拥有某地址的内存读写权限，但是该内存中的数据未初始化，或者不知道是否初始化过（注意，这时候从该地址读取数值的C标准中的UB，是不允许的！），那么可以用has_permission谓词。has_permission(px)表示拥有地址px的读写权限，但是这并不保证该地址上的数据是初始化过的。换言之，store(px, x)可以推出has_permission(px)，但是反过来has_permission(px)成立并不意味之存在一个值v使得store(px, v)。QCP中，has_permision也可以指定类型，例如has_permission(px, int)或者has_int_permission(px)。

值得一提的是，has_permission和store这两类谓词只能用于以下整数类型等基本类型、它们的指针类型或者它们的指针的指针类型等，而不能用于struct、union与数组等复合类型。

断言中的星号逻辑连接词

断言中的星号“*”是分离逻辑中的逻辑连接词“分离合取”。“P * Q”表示当前内存可以分为互不相交的两部分，其中一部分满足P另一部分满足Q。由此可以看出，store_int(px, x) * store_int(py, y)就说明了px与py是不同的地址。

我们在表述C程序规约时，常常会写多个（大于等于三个）子句的分离合取，而不仅仅时两个子句的分离合取。以三个子句的情况为例，“(P * Q) * R”表示内存可以分为互补相交的两部分，其中第一部分又可以分为更小的互不相交的两部分，也就是两两互不相交的三部分，它们分别满足性质P、Q和R。因此，不难看出，分离合取（即QCP中的星号“*”）具有交换律和结合律。以断言store(px, x) * store(py, y) * store(pz, z)为例，它的含义是“px、py与pz是三个互不相同的内存地址并这三个地址上存储的数值是x、y和z”，并且在书写时也不需要为前一个星号或者后一个星号添加额外的括号。