QCP Tutorials 内存与断言

如果C程序中a与b是两个有符号整数类型的全局变量，那么下面三种swap_ab函数都可以实现交换它们数值的效果。

int a;
int b;

void swap_ab()
{
  int t;
  t = a;
  a = b;
  b = t;
}

void swap_ab_alter1()
{
  swap(&a, &b);
}

void swap_ab_alter2()
{
  swap(&b, &a);
}

要描述这样的程序功能，可以使用全局变量的地址与分离逻辑谓词store一起构建Require条件和Ensure条件。

void swap_ab()
/*@ With x y
    Require store_int(&a, x) * store_int(&b, y)
    Ensure store_int(&a, y) * store_int(&b, x) */
;