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

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 是两个内存位置的初始内容：程序并不关心它们具体是多少，但后置条件需要提及它们才能表达“交换”的语义。目前的 C* 中，逻辑参数在调用点没有提供实参语法：符号执行引擎（下一节中介绍）会把被调用函数的 requirerequire 与调用点的符号状态（其实就是分离逻辑的空间断言）做匹配，自动推出逻辑参数的取值。

从资源的视角读这份契约：调用者把 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 由上一节的定义机制定义），契约只负责将堆与模型对应起来。

无函数体的契约：assumed spec

验证一个用 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——这正是“刚从内存中分配出来的结点”的准确刻画。

循环不变式

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 把整个函数的符号执行全部通过、看到全部验证条件，再回头逐个补证明。

用途二：`forfor` 与 `do-whiledo-while` 的手动不变式

[[cst::invariant]][[cst::invariant]] 只能用于 whilewhile 循环；forfor 与 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 指返回值；契约可标注于原型上；带契约而无函数体的原型是 assumed spec，属于信任基。
指针入参用逻辑参数命名初值（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]] 断言并替换一处的完整符号状态：在未写证明时可把资源改写成引擎需要的形态、先让符号执行完整通过（蕴含成为待证的验证条件），也为 forfor/do-whiledo-while 充当手动不变式。