函数契约、循环不变式与断言

EN | 中文

上一节介绍了如何在 C* 中书写空间断言，以及如何用定义机制为链表和树定义表示谓词。本节介绍如何在程序中使用这些断言：函数契约（Function Contracts）（[[cst::require]][[cst::require]]、[[cst::ensure]][[cst::ensure]]）、循环不变式（Loop Invariants）（[[cst::invariant]][[cst::invariant]]）与内联断言（Inline Assertions）（[[cst::assert]][[cst::assert]]）。断言可以用在这三类位置；写好之后，C* 就能沿程序逐句检查。

从求绝对值函数说起：契约的形式

回顾第一个 C* 程序中的求绝对值函数：


int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{ ... }


int myabs(int x)
  [[cst::require(`fact(x > --2147483648i)`)]]
  [[cst::ensure(`
      fact(
        (x >= 0i && __return == x) ||
        (x <  0i && __return == --x)
      )
  `)]]
{ ... }

前面已经见过契约的语法要素，这里正式说明各部分的含义：

契约写在参数表之后、函数体之前（对只有原型的声明，写在分号之前）；
[[cst::require(...)]][[cst::require(...)]] 是前置条件：函数开始执行时成立的断言，它刻画函数要操作的内存资源，并约束输入；
[[cst::ensure(...)]][[cst::ensure(...)]] 是后置条件：函数返回时成立的断言，它刻画返回时的内存资源，并用 __return__return 描述返回值；
契约中直接写参数名（如 xx），指的是参数在函数入口处的值。

契约约定了实现者的义务与调用者可以依赖的假设：实现者必须保证函数的每条返回路径都满足契约；调用者则无需阅读函数体，就能依赖契约推理。因此，检查调用点时只需查看契约，无需查看实现。

再看一个也只涉及栈上标量局部变量的例子，McCarthy 91 函数：


int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i && __return == n - 10i) ||
                   fact(n <= 100i && __return == 91i)`)]]
{
  if (n > 100) {
    return n - 10;
  };
  int r1 = mc91(n + 11);
  int r2 = mc91(r1);
  return r2;
}


int mc91(int n)
    [[cst::require(`fact(0i <= n)`)]]
    [[cst::ensure(`fact(n > 100i && __return == n - 10i) ||
                   fact(n <= 100i && __return == 91i)`)]]
{
  if (n > 100) {
    return n - 10;
  };
  int r1 = mc91(n + 11);
  int r2 = mc91(r1);
  return r2;
}

这个例子有两点值得注意。

其一，条件式后置条件：结论随输入而异时，用 |||| 分情况讨论，每个分支用 &&&& 将输入条件与空间断言合取（本例中都是空堆 factfact）。
其二，递归调用按同一契约检查：验证第 9 和 10 行的递归调用时，都只根据上面的契约推进；在 VSCode 中查看符号状态，就能观察 r1r1 和 r2r2 的取值情况。

后面讨论证明时，我们还会看到：契约必须足够强，否则递归调用处的证明可能无法推进。这与数学中的归纳证明类似：证明过程中常会发现，需要回头加强归纳假设。

指针参数

接下来用空间断言描述指针参数所指向的内存。一个经典例子是交换两个整数：


void swap(int *a, int *b)
    [[cst::param(`a_v:int`, `b_v:int`)]]
    [[cst::require(`data_at a Tint a_v ** data_at b Tint b_v`)]]
    [[cst::ensure(`data_at a Tint b_v ** data_at b Tint a_v`)]]
{
  int t = *a;
  *a = *b;
  *b = t;
}


void swap(int *a, int *b)
    [[cst::param(`a_v:int`, `b_v:int`)]]
    [[cst::require(`data_at a Tint a_v ** data_at b Tint b_v`)]]
    [[cst::ensure(`data_at a Tint b_v ** data_at b Tint a_v`)]]
{
  int t = *a;
  *a = *b;
  *b = t;
}

这里出现了第三种契约标注：[[cst::param(...)]][[cst::param(...)]] 声明逻辑参数（Logical Parameters），即只在逻辑层存在的额外参数。在本例中，a_va_v、b_vb_v 是两个内存位置的初始内容：程序无需关心它们的具体取值，但后置条件需要引用这些初值，才能表达“交换”的含义。逻辑参数通常无需在调用点传递：符号执行引擎（下一节中介绍）会把被调用函数的 requirerequire 与调用点的符号状态（即分离逻辑的空间断言）匹配，自动推断它们的取值。当匹配有歧义时，放在调用语句之前的标注 [[cst::where(`v`, `e`)]]` 可以显式给出一个逻辑实参，`[[cst::where_type(`:T`, `:ty`)]][[cst::where(`v`, `e`)]]` 可以显式给出一个逻辑实参，`[[cst::where_type(`:T`, `:ty`)]] 则用于类型参数。

从资源的角度看，调用者把 aa、bb 两个内存单元借给 swapswap，返回时收回这两个单元，其中的内容已经交换。注意指针参数 aa 在断言中直接用作地址，因为参数的值本身就是地址；后文循环不变式中的 __addr__addr 则表示局部变量自身所占内存单元的地址，两者需要区分。

指针的另一种常见角色是出参。比如，扩展欧几里得算法通过两个指针输出 Bézout 系数：


int ext_gcd(int a, int b, int *x, int *y)
    [[cst::require(`fact(0i <= a) ** fact(0i <= b) **
                    undef_data_at x Tint ** undef_data_at y Tint`)]]
    [[cst::ensure(`exists xv yv.
                    data_at x Tint xv ** data_at y Tint yv **
                    fact(a * xv + b * yv == __return) **
                    fact(b == 0i ==> xv == 1i && yv == 0i) **
                    fact(1i <= b ==> --b <= xv && xv <= b) **
                    fact(1i <= b ==> (--a <= yv && yv <= a) || yv == 1i)`)]]
{ ... }


int ext_gcd(int a, int b, int *x, int *y)
    [[cst::require(`fact(0i <= a) ** fact(0i <= b) **
                    undef_data_at x Tint ** undef_data_at y Tint`)]]
    [[cst::ensure(`exists xv yv.
                    data_at x Tint xv ** data_at y Tint yv **
                    fact(a * xv + b * yv == __return) **
                    fact(b == 0i ==> xv == 1i && yv == 0i) **
                    fact(1i <= b ==> --b <= xv && xv <= b) **
                    fact(1i <= b ==> (--a <= yv && yv <= a) || yv == 1i)`)]]
{ ... }

与 swapswap 对比，可以总结指针契约的两种模式：

入参（in-parameter）（调用前就有意义的值）：用逻辑参数命名初值，比如 data_at p Tint a_vdata_at p Tint a_v；
出参（out-parameter）（返回时才产生的值）：前置条件只要求一个可写内存单元 undef_data_at x Tintundef_data_at x Tint（内容可以是未初始化的），后置条件用存在量词（比如 exists xv yv.exists xv yv.）引入返回时的内容，再用 factfact 陈述其性质，比如这里的 a * xv + b * yv == __returna * xv + b * yv == __return。

后置条件的最后三条 factfact 用于为递归调用加强规约，并非调用者关心的结论。ext_gcdext_gcd 递归调用自身时，证明只能依赖这份契约，因此需要这些额外约束来完成函数体中的算术推理。递归函数的规约常常需要这样补充性质。

数组

数组的契约需要描述一段内存。上一节提到的 array_atarray_at 等谓词就用于此，但直接写入契约会受到符号执行引擎的一个限制（下一节详述）：契约与符号状态中，除 data_atdata_at/undef_data_atundef_data_at 之外的谓词不能直接携带 ctypectype 参数。目前建议用上一节介绍的定义机制，定义一个单态包装谓词，将 ctypectype 封装在定义体内。以“清零 nn 个字节”为例：


[[cst::proof]] thm undef_bytes_def = new_fun_definition(
    `undef_bytes (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_bytes`);
[[cst::proof]] thm zero_bytes_def = new_fun_definition(
    `zero_bytes (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zero_bytes`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{ ... }


[[cst::proof]] thm undef_bytes_def = new_fun_definition(
    `undef_bytes (x:addr) (n:int) : hprop = undef_array_at x Tchar n`);
[[cst::proof]] int _e1 = cst_add_const_to_header(`undef_bytes`);
[[cst::proof]] thm zero_bytes_def = new_fun_definition(
    `zero_bytes (x:addr) (n:int) : hprop = array_at x Tchar n (ireplicate n 0i)`);
[[cst::proof]] int _e2 = cst_add_const_to_header(`zero_bytes`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{ ... }

契约的含义是：给定从 arrarr 开始的 nn 个可写字节，函数结束时，这 nn 个字节的内容均为 00。其中 ireplicate n 0iireplicate n 0i（nn 个 0i0i 组成的列表）是逻辑层的纯函数。这是书写规约时的常用方法：用模型函数（model function）在纯数学值上描述结果，无需逐个枚举内存单元。后面链表与树的契约会进一步展示这种方法。

链表与树

数据结构的契约建立在上一节定义的表示谓词之上。原地反转单链表的契约只有三行：


[[cst::proof]] int _sll = cst_add_const_to_header(`sll`);
[[cst::proof]] int _rev = cst_add_const_to_header(`REVERSE:(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{ ... }


[[cst::proof]] int _sll = cst_add_const_to_header(`sll`);
[[cst::proof]] int _rev = cst_add_const_to_header(`REVERSE:(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{ ... }

逻辑参数 ll 是链表的逻辑内容（一个纯粹的 HOL 列表）；REVERSEREVERSE 是 HOL 列表库的现成函数。整份契约的含义是：输入一个内容为 ll 的链表，返回一个内容为 REVERSE lREVERSE l 的链表。实现可以采用任意方式反转链表，只要行为符合契约即可。多个逻辑参数之间用逗号分隔：拼接两个链表的函数可以声明 [[cst::param(`l1:(int)list`, `l2:(int)list`)]][[cst::param(`l1:(int)list`, `l2:(int)list`)]]，其契约是 sll p l1 ** sll q l2sll p l1 ** sll q l2 蕴含 sll __return (l1 ++ l2)sll __return (l1 ++ l2)。

树的契约同样如此。下面两个例子取自一个 AVL 树实现（store_treestore_tree、theighttheight、avl_insertavl_insert 分别是树的表示谓词与模型函数）：


// 把需要的类型和函数都通过 cst_add_const_to_header / cst_add_type_to_header 导出
// *out = nd 所指（可能为空的）子树的高度。
void node_height_p(struct tree *nd, int *out)
    [[cst::param(`t0:tree`)]]
    [[cst::require(`store_tree nd t0 ** undef_data_at out Tint`)]]
    [[cst::ensure(`store_tree nd t0 ** data_at out Tint (theight t0)`)]];
// AVL 插入：*root 所指的树由 t 变为 avl_insert k t。
void insert(struct tree **root, int k)
    [[cst::param(`t:tree`)]]
    [[cst::require(`exists pv.
                      data_at root Tptr pv **
                      store_tree pv t **
                      fact(theight t <= 2147483646i)`)]]
    [[cst::ensure(`exists qv.
                     data_at root Tptr qv **
                     store_tree qv (avl_insert k t) **
                     fact(theight (avl_insert k t) <= theight t + 1i)`)]];


// 把需要的类型和函数都通过 cst_add_const_to_header / cst_add_type_to_header 导出
// *out = nd 所指（可能为空的）子树的高度。
void node_height_p(struct tree *nd, int *out)
    [[cst::param(`t0:tree`)]]
    [[cst::require(`store_tree nd t0 ** undef_data_at out Tint`)]]
    [[cst::ensure(`store_tree nd t0 ** data_at out Tint (theight t0)`)]];
// AVL 插入：*root 所指的树由 t 变为 avl_insert k t。
void insert(struct tree **root, int k)
    [[cst::param(`t:tree`)]]
    [[cst::require(`exists pv.
                      data_at root Tptr pv **
                      store_tree pv t **
                      fact(theight t <= 2147483646i)`)]]
    [[cst::ensure(`exists qv.
                     data_at root Tptr qv **
                     store_tree qv (avl_insert k t) **
                     fact(theight (avl_insert k t) <= theight t + 1i)`)]];

这两个例子有以下几点值得注意。

这两份契约都标注在函数原型上（注意结尾的分号），因此规约可以写在头文件中。目前函数定义处仍需重复同一契约，可以用宏减少重复。将接口与规约放在一起符合 C 的惯例；C* 也建议用头文件组织多模块项目。
node_height_pnode_height_p 是只读函数：store_tree nd t0store_tree nd t0 在前后置条件中原样出现，表示函数借用这棵树，并在返回时原样归还。
insertinsert 的参数是二级指针：exists pv. data_at root Tptr pv ** store_tree pv texists pv. data_at root Tptr pv ** store_tree pv t 刻画 rootroot 所指的指针单元，以及该单元中的指针所指向的整棵树。
功能正确性由一次模型函数应用来描述：store_tree qv (avl_insert k t)store_tree qv (avl_insert k t)，即堆上实现的行为与模型在纯值上的行为一致。这就是“规约即模型”：用纯函数定义数据结构的行为（avl_insertavl_insert 由上一节的定义机制定义），契约只负责将堆与模型对应起来。

无函数体的契约：假定规约

验证使用 mallocmalloc（或其他标准库、外部库函数接口）的程序时，如果分配器本身没有契约，该怎么办？C* 支持带契约、无函数体的原型，称为假定规约（assumed spec）：


void malloc_node(struct tree **out)
    [[cst::require(`undef_data_at out Tptr`)]]
    [[cst::ensure(`exists nq.
                     data_at out Tptr nq **
                     fact(~(nq == 0i)) **
                     undef_data_at (field_addr nq Ttree Fkey) Tint **
                     undef_data_at (field_addr nq Ttree Fheight) Tint **
                     undef_data_at (field_addr nq Ttree Fleft) Tptr **
                     undef_data_at (field_addr nq Ttree Fright) Tptr`)]];


void malloc_node(struct tree **out)
    [[cst::require(`undef_data_at out Tptr`)]]
    [[cst::ensure(`exists nq.
                     data_at out Tptr nq **
                     fact(~(nq == 0i)) **
                     undef_data_at (field_addr nq Ttree Fkey) Tint **
                     undef_data_at (field_addr nq Ttree Fheight) Tint **
                     undef_data_at (field_addr nq Ttree Fleft) Tptr **
                     undef_data_at (field_addr nq Ttree Fright) Tptr`)]];

对它的调用照常按契约检查，但契约本身不经验证。这些契约属于信任基，应尽量减少数量、控制规模，并确保其正确性显而易见。注意，新分配的四个字段都用 undef_data_atundef_data_at 刻画（有内存，但未指定内容），再结合一条非空 factfact，就准确描述了刚分配的节点。

接收函数指针的函数也按同样的思路给出规约：在 requirerequire 中用常量 fnspecfnspec 给出契约，并假定指针所指的函数满足它；经由该指针的调用就按这份契约检查。

循环不变式

C* 的符号执行引擎沿程序逐句推进符号状态，但验证时并不知道循环体会执行多少次。按照霍尔逻辑的常规做法，需要我们提供一个循环不变式：一条在每次回到循环头时都成立的断言。它写在 while (...)while (...) 条件与循环体之间：


while (条件)
    [[cst::invariant(`...`)]]
{ 循环体 }


while (条件)
    [[cst::invariant(`...`)]]
{ 循环体 }

引擎按以下步骤使用不变式：进入循环前，检查它是否成立（建立）；假设它与循环条件同时成立，对循环体进行一次符号执行，检查它在循环体结束时重新成立（保持）；循环之后，以“不变式 + 条件为假”作为新的符号状态继续推进。循环头处，引擎只保留不变式。不变式未包含的资源和事实不会保留在后续的符号状态中，因此不变式必须完整描述循环头的符号状态。

从算术循环开始

先看一个纯标量的教学示例——Gauss 求和：


int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}


int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

循环不变式通常包含三类成分，这个例子中都能看到：

资源：用 data_atdata_at 描述每个活跃变量的存储单元。对于会变化的变量（ss、ii），用 existsexists 绑定其当前值 svsv、iviv；对于不变的变量（nn），直接写入口值 n__pren__pre。注意全部用的是显式地址形 __addr__addr/__pre__pre，不是程序变量名；这与 VSCode 展示的符号状态形式一致。
进度事实：2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i)——部分和公式，它在循环结束（iv == n__preiv == n__pre）时退化为后置条件。
边界事实：0i <= iv0i <= iv、iv <= n__preiv <= n__pre、n__pre <= 1000in__pre <= 1000i。前两条使我们能在循环退出时断定 iv == n__preiv == n__pre；最后一条来自前置条件。但前置条件不会在循环头自动保留，验证 s + is + i 不溢出时需要这条事实，因此必须将其一并纳入不变式。

遍历数组

回到前面的 clearclear 例子。如果用循环实现，就需要在不变式中刻画清零过程中的状态。为此，先定义一个包装谓词，描述尚未清零的后缀：


[[cst::proof]] thm undef_suffix_def = new_fun_definition(
    `undef_suffix (x:addr) (i:int) (n:int) : hprop =
       undef_array_at (x + i * sizeof Tchar) Tchar (n - i)`);
[[cst::proof]] int _e3 = cst_add_const_to_header(`undef_suffix`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists iv.
                          data_at i__addr Tint iv **
                          data_at n__addr Tint n__pre **
                          data_at arr__addr Tptr arr__pre **
                          zero_bytes arr__pre iv **
                          undef_suffix arr__pre iv n__pre **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(n__pre <= 2147483647i)`)]]
  {
    char *p = arr + i;
    *p = 0;
    i = i + 1;
  }
}


[[cst::proof]] thm undef_suffix_def = new_fun_definition(
    `undef_suffix (x:addr) (i:int) (n:int) : hprop =
       undef_array_at (x + i * sizeof Tchar) Tchar (n - i)`);
[[cst::proof]] int _e3 = cst_add_const_to_header(`undef_suffix`);
void clear(char *arr, int n)
    [[cst::require(`fact(0i <= n) ** undef_bytes arr n`)]]
    [[cst::ensure(`zero_bytes arr n`)]]
{
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists iv.
                          data_at i__addr Tint iv **
                          data_at n__addr Tint n__pre **
                          data_at arr__addr Tptr arr__pre **
                          zero_bytes arr__pre iv **
                          undef_suffix arr__pre iv n__pre **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(n__pre <= 2147483647i)`)]]
  {
    char *p = arr + i;
    *p = 0;
    i = i + 1;
  }
}

空间部分是遍历类不变式的标准形态：已处理前缀 **** 未处理后缀——zero_bytes arr__pre ivzero_bytes arr__pre iv 加 undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre，两段拼接起来恰好是前置条件刻画的整段内存。每次执行循环体，都从后缀取出一个字节，将其清零后并入前缀，两段的分界线 iviv 因而向右移动一个字节。

undef_suffixundef_suffix 的定义还用到了一个实用技巧：后缀的基址在定义体里写成 x + i * sizeof Tcharx + i * sizeof Tchar。上一节说过，arr + iarr + i 这样的指针运算在逻辑中展开为 sizeofsizeof 形式，而断言与符号状态的匹配是语法性的。将这种形式封装在定义体中，既能保持不变式简洁，也便于符号执行引擎匹配执行中产生的地址。

这里还有一个问题：*p = 0*p = 0 要写的那一个内存单元，符号状态里并没有直接给出对应的 undef_data_atundef_data_at——它折叠在 undef_suffixundef_suffix 里，符号执行引擎执行到这一步时会报错。这正是本节末内联断言（或后续章节的证明代码）要解决的问题。

遍历链表：`reversereverse`

最后来看原地反转链表的完整程序。前面已经介绍过契约，现在关注其中的循环：


[[cst::proof]] int _app = cst_add_const_to_header(`APPEND:(A)list->(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = 0;
  struct list *v = p;
  while (v != 0)
      [[cst::invariant(`exists wv vv l1 l2.
                          data_at p__addr Tptr p__pre **
                          data_at w__addr Tptr wv **
                          data_at v__addr Tptr vv **
                          sll wv (REVERSE l1) **
                          sll vv l2 **
                          fact(l == l1 ++ l2)`)]]
  {
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}


[[cst::proof]] int _app = cst_add_const_to_header(`APPEND:(A)list->(A)list->(A)list`);
struct list *reverse(struct list *p)
    [[cst::param(`l:(int)list`)]]
    [[cst::require(`sll p l`)]]
    [[cst::ensure(`sll __return (REVERSE l)`)]]
{
  struct list *w = 0;
  struct list *v = p;
  while (v != 0)
      [[cst::invariant(`exists wv vv l1 l2.
                          data_at p__addr Tptr p__pre **
                          data_at w__addr Tptr wv **
                          data_at v__addr Tptr vv **
                          sll wv (REVERSE l1) **
                          sll vv l2 **
                          fact(l == l1 ++ l2)`)]]
  {
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }
  return w;
}

这个不变式表示：任一时刻，原链表分为两段——ww 指向已反转的前缀（内容 REVERSE l1REVERSE l1），vv 指向尚未处理的后缀（内容 l2l2）；纯事实 l == l1 ++ l2l == l1 ++ l2 把两段与原链表联系在一起。

reversereverse 不变式的示意图：已反转前缀（内容 REVERSE l1REVERSE l1）与未处理后缀（内容 l2l2），fact(l == l1 ++ l2)fact(l == l1 ++ l2) 将两段与原链表联系起来。

下面按引擎的三个步骤检查这个不变式：

建立：进入循环前 w == 0w == 0、v == pv == p，取 l1 = []l1 = []、l2 = ll2 = l——空前缀（空列表）反转后仍为空列表（sll 0i (REVERSE [])sll 0i (REVERSE []) 即空堆），后缀是整条链表，l == [] ++ ll == [] ++ l 显然成立。
保持：v != 0v != 0 时后缀非空。循环体先在证明块中按 sllsll 的定义展开头节点，得到 headhead、tailtail 两个单元的 data_atdata_at；接着 v->tail = wv->tail = w 将头节点连接到已反转的前缀，ww、vv 均向前移动；最后以 l1' = l1 ++ [头元素]l1' = l1 ++ [头元素]、l2' = 尾部l2' = 尾部 重新折叠为两段 sllsll。v->tailv->tail 能执行，正是因为展开后，不变式中包含了该单元的 data_atdata_at。
出口：v == 0v == 0 时后缀是空列表，l2 == []l2 == []，于是 l1 == ll1 == l，ww 一侧的 sll wv (REVERSE l)sll wv (REVERSE l) 正是后置条件。

与数组一例相同，v->tailv->tail 所需的字段资源折叠在 sll vv l2sll vv l2 里，若不展开便执行则会报错。展开可以用证明代码完成，也可以用下面的内联断言先行推进。

不变式书写准则

完整：不变式必须描述循环头的全部符号状态——每个活跃变量的 data_atdata_at（或 undef_data_atundef_data_at）、每块堆资源、后续还要用的每条 factfact。引擎在循环头只保留不变式。
显式地址形：用 __addr__addr、__pre__pre 书写，不要用程序变量名直接引用内存。
变化的量用 existsexists：绑定名（iviv、wvwv……）不得与任何程序变量同名。
入口可建立：进入循环前，符号状态必须能以精确实例化的形式匹配不变式（如 reversereverse 中取 l1 = []l1 = []、l2 = ll2 = l 的那一步）。
解引用可见：循环条件与循环体要解引用的内存，必须在不变式中以 data_atdata_at 或其他自定义表示谓词的形式呈现。

内联断言

最后一个标注是 [[cst::assert(`...`)]][[cst::assert(`...`)]]：作为一条语句写在函数体内，断言此处的符号状态。引擎处理它分两步：先检查当前符号状态蕴含所断言的状态，这个蕴含成为一个验证条件；然后以所断言的状态为新的符号状态继续推进。通过改写符号状态并继续执行，assertassert 有以下两种用途。

用途一：改写符号状态，推进符号执行

前面 clearclear 与 reversereverse 的循环体都还无法直接完成符号执行：不变式里的资源是折叠形态（undef_suffixundef_suffix、sll vv l2sll vv l2），而 *p = 0*p = 0 要写的是 pp 所指的那个单元、v->tailv->tail 要读的是节点的 tailtail 字段——符号状态里并未直接给出这些 data_atdata_at/undef_data_atundef_data_at 资源，符号执行引擎在这两处会报错。按定义展开谓词需要证明代码（后续章节介绍）。在尚未编写证明时，可以先插入一条 assertassert，将符号状态改写为展开一步后的形态，让符号执行继续。clearclear 的循环体可以写为：


  {
    char *p = arr + i;
    [[cst::assert(`exists iv.
        fact(0i <= iv && iv < n__pre && n__pre <= 2147483647i) **
        data_at p__addr Tptr (arr__pre + iv * sizeof Tchar) **
        data_at i__addr Tint iv **
        data_at n__addr Tint n__pre **
        data_at arr__addr Tptr arr__pre **
        zero_bytes arr__pre iv **
        undef_data_at (arr__pre + iv * sizeof Tchar) Tchar **
        undef_suffix arr__pre (iv + 1i) n__pre`)]];
    *p = 0;
    i = i + 1;
  }


  {
    char *p = arr + i;
    [[cst::assert(`exists iv.
        fact(0i <= iv && iv < n__pre && n__pre <= 2147483647i) **
        data_at p__addr Tptr (arr__pre + iv * sizeof Tchar) **
        data_at i__addr Tint iv **
        data_at n__addr Tint n__pre **
        data_at arr__addr Tptr arr__pre **
        zero_bytes arr__pre iv **
        undef_data_at (arr__pre + iv * sizeof Tchar) Tchar **
        undef_suffix arr__pre (iv + 1i) n__pre`)]];
    *p = 0;
    i = i + 1;
  }

与不变式对照，这条 assertassert 做了三件事：把循环条件带来的 iv < n__preiv < n__pre 写进 factfact（进入循环体后它已成立）；补上新声明的 pp 的资源（其值正是 sizeofsizeof 形的地址）；其中最关键的是，将 undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre 分解为头字节 undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar 加余下后缀 undef_suffix arr__pre (iv + 1i) n__preundef_suffix arr__pre (iv + 1i) n__pre。 assertassert 之后，符号状态中已经明确包含了 *p*p 所需的单元资源，符号执行就能通过这一步。类似地，reversereverse 的循环体在读 v->tailv->tail 之前，用 assertassert 把 sll vv l2sll vv l2 展开成头节点的两个单元加余下链表（vvvv 非空，故 l2l2 必为某个 x :: xsx :: xs）：


  {
    [[cst::assert(`exists q x xs l1 vv wv.
        fact(~(vv == 0i) && l == l1 ++ x :: xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr wv **
        data_at v__addr Tptr vv **
        sll wv (REVERSE l1) **
        data_at (field_addr vv Tlist Fhead) Tint x **
        data_at (field_addr vv Tlist Ftail) Tptr q **
        sll q xs`)]];
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }


  {
    [[cst::assert(`exists q x xs l1 vv wv.
        fact(~(vv == 0i) && l == l1 ++ x :: xs) **
        data_at p__addr Tptr p__pre **
        data_at w__addr Tptr wv **
        data_at v__addr Tptr vv **
        sll wv (REVERSE l1) **
        data_at (field_addr vv Tlist Fhead) Tint x **
        data_at (field_addr vv Tlist Ftail) Tptr q **
        sll q xs`)]];
    struct list *t = v->tail;
    v->tail = w;
    w = v;
    v = t;
  }

不过，“旧状态蕴含所断言的状态”仍是一个待证的验证条件（此处正是按定义展开 undef_suffixundef_suffix/sllsll 的那一步）。assertassert 并未消除证明义务，而是让符号执行先继续，将这一义务留待后续证明。这是 C* 中一种实用的工作流：先用 assertassert 完成整个函数的符号执行，查看全部验证条件，再逐个补充证明。

为不变式的例证命名：[[cst::given]][[cst::given]]

循环体内的 assertassert 常常需要引用不变式中的存在例证，但这些名字由不变式的 existsexists 绑定，对循环体内的标注不可见。语句 [[cst::given(`k:int`, `xv:int`)]];[[cst::given(`k:int`, `xv:int`)]];（注意末尾的 ;;）按指定名字绑定当前符号状态中的存在变量，同一语句块中位于它之后的标注便可以直接引用 kk 与 xvxv。下面的循环里，不变式对剩余距离 kk 做了存在量化，使用 givengiven 后，断言就能描述循环条件成立时它仍为正这一性质：


while (x < n)
  [[cst::invariant(`exists k xv.
      data_at n__addr Tint n__pre **
      data_at x__addr Tint xv **
      fact(xv + k == n__pre && 0i <= xv && 0i <= k) **
      fact(0i <= n__pre && n__pre <= 1000i)`)]]
{
  [[cst::given(`k:int`, `xv:int`)]];
  [[cst::assert(`data_at n__addr Tint n__pre ** data_at x__addr Tint xv **
      fact((xv + 1i) + (k - 1i) == n__pre && 0i <= xv && k >= 1i) **
      fact(0i <= n__pre && n__pre <= 1000i)`)]];
  x = x + 1;
}


while (x < n)
  [[cst::invariant(`exists k xv.
      data_at n__addr Tint n__pre **
      data_at x__addr Tint xv **
      fact(xv + k == n__pre && 0i <= xv && 0i <= k) **
      fact(0i <= n__pre && n__pre <= 1000i)`)]]
{
  [[cst::given(`k:int`, `xv:int`)]];
  [[cst::assert(`data_at n__addr Tint n__pre ** data_at x__addr Tint xv **
      fact((xv + 1i) + (k - 1i) == n__pre && 0i <= xv && k >= 1i) **
      fact(0i <= n__pre && n__pre <= 1000i)`)]];
  x = x + 1;
}

这些名字必须与状态中存在变量的名字完全一致，绑定持续到语句块结束，givengiven 本身不产生验证条件。只有由编译器在 C 作用域中处理的标注才需要它，比如 assertassert、wherewhere 或内层循环的不变式；后面章节介绍的证明块无需 givengiven 就能访问这些例证。

用途二：循环体内的手动不变式

[[cst::invariant]][[cst::invariant]] 同样可以附加在 forfor 与 do-whiledo-while 循环上（只有一条限制：forfor 的头部不能声明变量，应写成 int i; for (i = 0; …)int i; for (i = 0; …)）；对 do-whiledo-while，不变式在判断处、也就是循环体之后检查。也可以在同一位置手动插入一条 assertassert，充当“手动不变式”，如下例所示：


int mul(int x, int y)
    [[cst::require(`fact(1i <= x && x <= 100i) **
                    fact(1i <= y && y <= 100i)`)]]
    [[cst::ensure(`fact(__return == x * y)`)]]
{
  int ans = 0;
  do {
    ans += y;
    x--;
    [[cst::assert(`exists xv av.
        data_at x__addr Tint xv **
        data_at y__addr Tint y__pre **
        data_at ans__addr Tint av **
        fact(1i <= x__pre && x__pre <= 100i &&
             1i <= y__pre && y__pre <= 100i) **
        fact(0i <= xv && xv <= 99i) **
        fact(av + xv * y__pre == x__pre * y__pre)`)]];
  } while (x > 0);
  return ans;
}


int mul(int x, int y)
    [[cst::require(`fact(1i <= x && x <= 100i) **
                    fact(1i <= y && y <= 100i)`)]]
    [[cst::ensure(`fact(__return == x * y)`)]]
{
  int ans = 0;
  do {
    ans += y;
    x--;
    [[cst::assert(`exists xv av.
        data_at x__addr Tint xv **
        data_at y__addr Tint y__pre **
        data_at ans__addr Tint av **
        fact(1i <= x__pre && x__pre <= 100i &&
             1i <= y__pre && y__pre <= 100i) **
        fact(0i <= xv && xv <= 99i) **
        fact(av + xv * y__pre == x__pre * y__pre)`)]];
  } while (x > 0);
  return ans;
}

与 invariantinvariant 一样，assertassert 断言的是该程序点的完整符号状态，前一节的书写准则同样适用。

小结

函数契约 = [[cst::require]][[cst::require]] + [[cst::ensure]][[cst::ensure]]（辅以 [[cst::param]][[cst::param]] 逻辑参数），写在参数表之后；契约中参数名指入口值，__return__return 指返回值；契约可标注于原型上；带契约而无函数体的原型是假定规约，属于信任基。
指针入参用逻辑参数命名初值（data_at p Tint a_vdata_at p Tint a_v）；出参在前置条件中用 undef_data_atundef_data_at 描述可写单元，在后置条件中用 existsexists 引入新值。
数组契约用单态包装谓词隐藏 ctypectype（引擎限制）；契约中出现的新常量、新类型须导出（cst_add_const_to_headercst_add_const_to_header/cst_add_type_to_headercst_add_type_to_header）。
数据结构契约 = 表示谓词 + 模型函数：堆上实现的行为与模型在纯值上的行为一致。
循环不变式描述循环头的完整符号状态；遍历类的标准形态是“已处理前缀 **** 未处理后缀”，并包含进度与边界 factfact；书写时应遵循上述五条准则。
[[cst::assert]][[cst::assert]] 断言并替换一处的完整符号状态：在未写证明时可把资源改写成引擎需要的形态、先让符号执行完整通过（蕴含成为待证的验证条件），也可以在循环体内充当手动不变式。
匹配有歧义时，[[cst::where]][[cst::where]] 在调用处显式传入一个逻辑实参；[[cst::given]][[cst::given]] 为当前状态的存在例证命名，使 assertassert、wherewhere 或内层循环的不变式能够提到它们。