本手册是安全C语言的规范语言SCSL（Safe C Specification Language）的参考手册(PDF文档)，供熟悉ISO C编程语言，有些了解安全C语言，并准备用安全C语言的验证器－科创SC验证器，进行程序验证的软件技术人员学习如何描述程序功能时使用。
　　SCSL是安全C语言的行为接口规范语言（behavioral interface specification languages），可用来编写程序标注，程序标注加在程序注释中，用来描述安全C源代码的行为性质，因此SCSL又简称为标注语言。该语言的设计参考了ACSL语言（ANSI/ISO C Specification Language）[1]，也体现出了中国科学技术大学计算机学院相关实验室多年来的的研究成果[2, 3, 5]。
　　源文件中很多地方都有标注，这些标注是对相关程序片段行为的描述，它们综合起来就构成程序行为的描述。 从宏观上看，标注分成两大部分：全局标注和语句标注。

　　全局标注 主要有下面几种。

1. 函数协议
   描述函数的行为，其标注正好插在函数的声明或定义之前。
2. 类型不变式
   描述结构体和共用体等类型的不变性，其标注正好出现在被描述对象的定义或声明之后。
3. 变量不变式
   描述外部变量，静态外部变量和静态局部变量的不变性也是出现在对应的全局或局部声明的层次上 。
4. 全局逻辑声明
   逻辑的常量、类型、变量、函数、谓词及引理等的定义或声明可标注在允许全局声明出现的地方有些也可以出现在允许局部声明出现的地方 。

1. 程序点断言
   程序点断言标注在C标号可以出现的任何地方，或者正好在程序块的闭括号之前，描述该程序点状态必须满足的断言。
2. 循环标注
   循环标注有循环不变式和循环变式，它们出现在 for、while 和 do…while 循环语句之前。
3. 幽灵代码
   幽灵代码是正规的C代码，可以有幽灵变量声明、结构体的幽灵域声明和幽灵赋值语句等它们标注在变量声明、域声明和赋值语句等可以出现的地方。幽灵变量和幽灵语句的引入有助于书写标注。幽灵代码仅能出现在标注中，并且它们只能修改幽灵变量。

　　与ACSL 和其他标注语言不同，仅SCSL 特有的部分是易变数据结构的形状标注。它是依据形状图逻辑和形状系统[2]，形状图理论的定理证明[5]，以及上述全局标注和语句标注等的设计而设计出来的。在程序验证中，形状声明标注即有助于程序员在函数前后断言、循环不变式和程序点断言中描述单态和多态命名基本形状中各节点的指针特性，也有助于程序验证系统发现程序中的指针错误。SCSL 所提供的易变数据结构的形式定义、它们的归纳引理和非归纳引理等的描述方式，方便了操作易变数据结构的程序的验证。

　　重要备注：对于《安全C语言使用手册》第三章介绍为易变数据结构设计的形状系统，目前仅实现3.1节介绍的单态命名基本形状。因此本手册中有关其它形状的描述和例子在实现过程中可能还会修改。

　　本篇是安全C的规范语言SCSL（Safe C Specification Language）的参考手册。SCSL 是安全C 语言的行为接口规范语言（behavioral interface specification languages），可用来规范安全C源代码的行为性质。该语言的设计参考了ACSL 语言（ANSI/ISO C Specification Language）[1]，也体现出了中国科学技术大学计算机学院相关实验室先前的研究成果[2, 3]。
　　本文档认为读者熟悉ISO C 编程语言，比较了解安全C 语言。

1.1 标注概述

1.2 标注的语法设计

　　程序的规范是以标注的形式直接写在C源文件的注释中，以保持源文件仍然可编译。作为标注的注释必须以 /*@ 开始并以 */ 结束，或者以 //@ 开始到本行结束。这类注释中的其余部分都被认为是标注。源文件中很多地方都有标注，这些标注是对相关程序片段行为的描述，它们综合起来就构成程序行为的描述。因此规范语言也称为标注语言。
　　全局逻辑声明和定义，例如谓词定义和逻辑函数定义等，其作用域是所在文件。若需要被多个文件共享，则可用文件包含的方式，让它们出现在这些文件都包含的头文件中。
　　标注分成全局标注和语句标注两类。其中

　　全局标注有下面几种。

1. 函数协议
   包含函数协议的标注正好插在函数声明或定义之前。
2. 类型不变式
   类型不变式可用于描述结构体和共用体等类型的不变式，其标注正好出现在被描述对象的定义或声明之后。
3. 变量不变式
   变量不变式可用于全局变量，也可用于静态外部变量和静态局部变量。例如一个整型静态局部变量b，在其生存期内始终不会小于0，则可以为它标注不变式 b >= 0。变量不变式的标注正好出现在变量声明之后。
4. 形状声明
   形状声明用来表达自引用结构体类型（也可能是其他类型）用来构造哪类形状的易变数据结构。形状声明的标注正好出现在相应的类型声明之后。
5. 全局逻辑声明
   逻辑的常量、类型、变量、函数、谓词及引理等的定义或声明可以标注在允许全局声明出现的地方。有些也可以出现在允许局部声明出现的地方。

1. 程序点断言
   程序点断言可标注在C 标号可以出现的任何地方，或者正好在程序块的闭括号之前。
2. 循环标注
   循环标注有不变式和变式，它们可以出现在 for、while 和 do…while 循环语句之前。
3. 幽灵代码
   幽灵代码是正规的C 代码，可以有幽灵变量声明、结构体的幽灵域声明和幽灵赋值语句等，它们标注在变量声明、域声明和赋值语句等可以出现的地方。幽灵代码仅能够被规范所访问，并且它们只能修改幽灵变量。

　　标注的文法必须仔细设计，以避免标注和代码相互影响。例如，在如下的代码中

if (c) //@ assert P;
    c = 1;

　　词法结构绝大部分遵从ANSI C。少数区别必须注意。

1. 在注释 /*@... */ 和 //@... 中这两个位置的@ 符号仅表示本注释是标注。
2. 标识符可以由反斜线字符开始，但是仅限于内建的谓词和函数等。
3. 某些UTF8 字符可用来代替某些逻辑或算术算符，它们列在表2.1中。（暂未实现）
4. 注释也可以出现在SCSL的标注中，它们只能使用以 // 开始到当前行结束的形式。

　　本节展示在标注中用的表达式，称为逻辑表达式。图3.1和图3.2给出逻辑表达式基本构造的文法。

　　在此文法中，逻辑表达式分为项和断言，项 对应到一阶逻辑的项，断言 对应到一阶逻辑的命题和谓词，并遵循它们在一阶逻辑中的通常区别。项对应到C语言中无副作用的表达式，另外，项还增加了一些算符和构造，其中由“\”开始的标识符都是系统内建的。
　　逻辑表达式是关于程序变量的性质断言，因此程序变量可以出现在逻辑表达式中，只要它们在逻辑表达式出现程序点是可见的。在第7章和第9章还会引入逻辑变量和幽灵变量，它们也可以出现在逻辑表达式中。

　　下面列出大部分新增的算符和构造，其余的在本章各节陆续介绍。

1. 新增逻辑连接词
   C的算符&&（UTF8: ∧）、||（UTF8: ∨）和!（UTF8: ¬）作为逻辑连接词，新增逻辑连接词有 蕴涵==>（UTF8: ⇒）、等价<==>（UTF8: ⇔）和 异或^^（UTF8: ⊕）。这些逻辑连接词都有按位运算的对应算符，或者是C本身有的（&、|、~和^），或者是新增的（--> 和 <-->。按位蕴涵和按位等价，暂未实现）。

　　图3.2中的终结符 id、C-type-name 以及各种字面常量就是C中对应的词法记号。

2. 连续的比较运算
   带若干个连续比较算符的构造 t₁ relop₁ t₂ relop₂ t₃ … t_k 是(t₁ relop₁ t₂) && (t₂ relop₂ t₃) && … && (t_k-1 relop_k-1 t_k) 的缩写。它要求所有的算符 relop_i 是同一个“方向”的，即都属于 {<, <=, ==} 或者都属于 {>, >=, ==}。像 x < y > z 和 x != y != z 这样的表达式是不允许的。

int f(int const a, int const b) { return a < b; }

• 先前已经提到，\result == a < b 不是正确的后条件，因为它是 \result == a && a < b 的缩写。
• 先前也提到，从C语言表达式的语义看，\result == (a < b) 是正确的后条件。但逻辑表达式语言不接受这样的断言，因为 a < b 是布尔类型，\result 是整型，两者之间没有隐式的类型转换。
• 同样，\result == (integer)(a < b) 在此作为后条件也是不合适的，因为逻辑表达式中没有这样的显式类型转换。写成 \result == (a < b ? 1 : 0) 是可以的。
• (\result != 0) == (a < b) 是不依赖于转换的等价后条件，这是可接受的后条件，两对括号都是必不可少的。
• \result != 0 <==> a < b 也是可接受的后条件，因为它是两个断言之间的等价。

3. 量化
   全称量化 由 \forall τ x.e 或 \forall τ x:[a₁…b₁, …, a_n…b_n].e 表示，存在量化 由 \exists τ x.e 或 \exists τ x:[a₁…b₁, …, a_n…b_n].e 表示。
   对于前者（即没有区间描述的情况），其中x 是τ 类型的约束变元，τ 可以是任何逻辑类型和C的类型。没有区间描述时，全称则表示对类型τ 的所有元素，存在量化则表示存在类型τ 的一个元素。对于后者，各个a_i 和b_i 是类型τ 的表达式，表示一个区间。对于可以使用区间的类型，可以出现多个区间。全称量化和存在量化这时分别表示类型τ 在这些区间中的所有元素和在这些区间中存在一个元素。
4. 条件表达式和条件断言
   它们的语法形式一样，都是 c ? e₁ : e₂ 。它可以是布尔类型的项或逻辑断言。在断言情况下，构造 c ? e₁ : e₂ 的两个分支 e₁ 和 e₂ 都必须是断言，使得它的语义等价于 (c ==> e₁) && (!c ==> e₂)。
5. 逻辑函数
   逻辑函数和谓词在项和断言中的应用不同于C的函数应用，详见第7章。
6. 图3.1和图3.2中以反斜线开始的内建函数在后面相关章节中介绍。还有一些内建函数和谓词没有在图3.1和图3.2中列出，它们大部分在讨论实数和浮点数的3.5节中介绍。

3.1 算符优先级

3.2 语义

3.3 定型

3.4 整数算术和机器整数

3.5 实数和浮点数

3.5.1 实数与浮点数的联系与区别

3.5.2 对浮点计算程序的验证

3.6 数组和指针

3.7 结构体、共用体和数组

3.8 字符串

　　C的算符优先级 在此得到保持，这里还需要加入新增算符，列在表3.1中。在该表中，算符按照优先级从高到低次序排列。同样优先级的算符则列在同一行。

　　SCSL逻辑表达式的语义 基于一阶数理逻辑，它是仅有全函数而无部分函数的二值逻辑。表达式绝不会没有定义，这是一个重要的设计选择，规范的书写者必须知道这一点。
　　因为仅有全函数，这意味着可以写诸如 1/0 和 *p（其中 p 是NULL 或悬空指针）的项。特别是，断言 1/0 == 1/0 和 *p == *p 是合法的，因为它们是一阶逻辑中公理 ∀x, x = x 的实例。不必为此担心，因为从这样的断言不可能演绎出任何有用的东西。像通常情况一样，书写无矛盾的断言取决于规范的设计者。例如，当引入下面引理时，y 不能为零的前提应该加上。

/*@ lemma div_mul_identity:
　　\forall real x. \forall real y. y != 0.0 ==> y*(x / y) == x;
*/

　　逻辑表达式语言 是一种类型化的语言。它包含C的类型和逻辑类型。逻辑类型由下面两点定义。

• 数学类型：无界的整数 integer 和实数 real，还有布尔类型 boolean（其值为 \true和 \false）。
• 由程序规范的书写者引入的逻辑类型。见第7章。

• C的整数类型 char、short、int、long 和 long long，无论有符号或无符号，都是类型 integer 的子类型。
• 类型 integer 是类型 real 的子类型。
• C的类型 float 和 double 都是类型 real 的子类型。

• 布尔类型和断言类型有区别。在项的位置出现的表达式 x < y 是布尔型的，而同样表达式出现在断言的位置则是断言类型的。
• 和C不一样的是，这里不存在 integer 和 boolean 两类型之间的隐式强制，也不允许两者之间有显式类型强制。
• 先前已经提到，可以对任何逻辑类型和C类型进行量化，以得到量化断言。
• 对于量化断言，具有区间限制的约束变元的类型必须是整数类型或枚举类型。

　　加、减、乘和一元减 这些算术运算都可用于数学整型 integer。C整数类型的变量的值被提升为数学整数类型。因此在逻辑表达式中没有算术溢出。
　　除运算和模运算也是数学运算，它们与对应的C 运算在C 机器整数上一致，因此遵循ISO C99 的习惯，不是通常的数学上欧几里德带余数的除法。一般而言，在有余数的情况下，除的结果取靠近0的值。若除数为0，则结果没有说明；其余情况下，若 q 和 r 分别是 n 除以 d 的商和余数，则：

• |d × q| ≤ n，|q| 对这个性质来说是最大的；
• 如果 |n| < |d|，那么 q 是0；
• 如果 |n| ≥ |d| 并且 n 和 d 有同样的符号，则 q 是正的；
• 如果 |n| ≥ |d| 并且 n 和 d 有相反的符号，则 q 是负的；
• d × q + r = n；
• |r| < |d|；
• r 等于0 或者与 n 有同样的符号。

• 5/3 是 1，5%3 是 2；
• (-5)/3 是 -1，(-5)%3 是 -2；
• 5/(-3) 是 -1，5%(-3) 是 2；
• (-5)/(-3) 是 1，(-5)%(-3) 是 -2。

/*@ ensures \result <= sizeof(int); */
    int f() { return sizeof(char); }

• 7 & 12 == ...00111 & ...001100 == ...00100 == 4
• -8 | 5 == ...11000 | ...00101 == ...11101 == -3
• ~5 == ~...00101 == ...111010 == -6
• -5 << 2 == ...11011 << 2 == ...11101100 == -20
• 5 >> 2 == ...00101 >> 2 == ...0001 == 1
• -5 >> 2 == ...11011 >> 2 == ...1110 == -2

　　浮点计算程序的验证 分成两步来学习。

1. 暂不涉及计算精度的验证
   但关注代码计算过程的正确性，即验证得到的结果与被验证代码在机器上的计算结果一致。
2. 增加计算精度的验证，完善浮点计算的验证。

　　浮点常数及其上的运算 解释为数学实数及其上运算。这样，出现在断言语言中的C语言浮点型和双精度型的常量和变量都隐式地提升为实型常量和变量。必要时，integer 类型的常量和变量也提升为 real 类型的常量和变量。通常的二元运算都解释成实数上的运算，在这样的情况下，计算不会出现任何舍入或溢出。
　　例如，在逻辑表达式中，1e+300 * 1e+300 等于 1e+600，即使 1e+600 大于双精度所能表示的最大数也不必在意，因为没有溢出。2*0.1 等于实数0.2，而不是等于它的浮点近似，因为不存在“舍入”。
　　和把C的整数类型提升到数学整数相比，对于浮点类型，不一样的地方是，它有3个特殊浮点数是不能自然地映射到实数的，即IEEE 754中作为“非数”（NaN：not a number）、+∞ 和 -∞ 的特殊值。稍后对这些特殊值有详细讨论。SCSL逻辑只有全函数，但有一个例外，隐式提升函数对“非数”、+∞ 和 -∞ 这3个值没有规定结果。
　　在逻辑表达式中，实数也可以用C99的16进制表示法，即 0xhh.hhp±dd，其中h 是16进制数字，d 是10进制数字，0xhh.hhp ± dd 表示 hh.hh × 2^±dd，例如 0x1.Fp-4 是 (1+15/16) × 2^-4。
　　常见的比较运算符 ==、!=、<、<=、> 和 >= 可用于real 、double 和float 类型，也就是它们是重载的算符，对于不同类型的运算对象，它们被解释成相应类型上的运算。 其实，float 和double 类型上的这些比较运算的结果，与把它们隐式提升到real 类型后，在real 类型上的比较结果是一样的。
　　从C的整数类型或单精度类型到单精度类型或双精度类型的强制和C中做法的一样，即应用同样的转换操作。但是，从实数到单精度或双精度值的转换依赖于由IEEE 754 标准定义的不同的舍入模式。这些舍入模式可以由一个内建的逻辑类型来定义。先给出相关类型。

/*@ type sign = \Positive | \Negtive;
    logic sign \sign(float x);
    logic sign \sign(double x);
*/

　　验证计算结果的精度，是浮点计算程序验证的重要内容。在目前不提供计算结果的精度验证情况下，可以从下面几方面学习浮点程序的验证。

1. 可以验证函数代码实现的算法是否与标注所描述的抽象算法一致。

// 例3.6　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include<limits.h>
//@logic double sum(double* arr, int n) = n < 0 ? (double)0.0 : sum(arr, n-1) + arr[n];

/*@	requires 0 <= n <= INT_MAX && \length(arr) == n; 
	ensures \result == sum(arr, n-1) && \length(arr) == n;
*/
double fsum(double* const arr, const int n){
	int i;  double ret;  ret = 0.0;

	//@loop invariant 0 <= i <= n <= INT_MAX && \length(arr) == n && ret == sum(arr, i-1); 
	for(i = 0; i < n ; i++){
		ret = ret + arr[i];
	}
	return ret;
}
					图3.3 对arr[0] + … + arr[n-1]求和的代码和标注

2. 代码中有浮点常数时，对计算结果的关注不同，能否验证则也可能不一样。下面的例3.7讨论的是能否按浮点计算的语义，验证代码的计算结果是正确的。

// 例3.7　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include<limits.h>

//@logic float clockSum(int n)= n <= 0 ? (float)0.0 : (float)(clockSum(n-1) + (float)0.1);

// 函数1
/*@	requires 0 <= n <= INT_MAX;
	ensures \result == clockSum(n);
*/
float clock_single1(const int n){
	float t; int i;

	//@ loop invariant 0 <= i <= n <= INT_MAX && t == clockSum(i) && !\is_infinite(t);
	for (i = 0, t = 0.0f; i < n; i++){
		t = t + 0.1f;
	}
	return t;
}

// 函数2
/*@	requires 0 <= n <= INT_MAX;
	ensures \result == (float)(0.1 * n);
*/
float clock_single2(const int n){
	float t; int i;
	//@ loop invariant 0 <= i <= n <= INT_MAX && t== (float)(0.1 * i) && !\is_infinite(t);
	for (i = 0, t=0.0f; i < n; i++) {
		t = t + 0.1f;
	}
	return t;
}
					图3.4 同样方式计算 0.1f*n，但验证的目标不一样

// 例3.8
#include <stdio.h>
int main(){
	double u = 2.0;
	double v = -4.0;
	double w;
	int i;
	int max = 31;
	for(i = 3; i <= max; i++){
		w = 111.- 1130./v + 3000./(v*u);
		u = v; v = w;
		printf("u%d = %1.17g\n", i, v);
	}
	return 0;
}
	图3.5 迭代计算未得正确结果的例子

3. 在目前不提供计算结果的精度验证情况下，由于机器误差的存在，一般来说，迭代计算的浮点程序的具体结果值是验证不了的。举一个典型的例子。

　　取地址算符、数组访问、指针算术和指针脱引用运算 类似于它们在C 中对应的运算。由于逻辑语言中没有指针类型，因此指针在断言语言中的使用一定受到限制。在这样的限制下，指针被看成是整型的。
　　先说指向栈区或静态数据区的指针，注意，数组名也是指针。取地址运算的使用必须小心，在逻辑表达式中取地址运算得到的是不依赖于C内存的一个抽象值而不是具体值，根据安全C语言的规定，取地址算符的使用范围大大缩小。
　　对于指针p 和q ，限定必须用 p == q、或 p == q ± e 这样的断言来表示p 和q 指向同一个数据块（其中e 是整型表达式），同时表示它们的大小关系。否则p 和q 被认为指向不同的数据块或者指针关系断言不合要求。上面的限定同时体现出不允许对 p 和 q 进行加减乘除和比较等其他运算（虽然 q - p == e 本质上就是 p == q - e）。p != q（或 !(p == q)）表示两个指针不相等，它用来表示 p 和 q 指向不同的数据块。指向同一个数据块但并不相等的 p 和 q 用 p == q ± e 方式表示。同样，!( p == q ± e)（或 p != q ± e）也仅表示 p 和 q 指向不同的数据块。
　　指向不同数据块的指针进行相等与否比较和大小比较毫无意义，其它操作更是免谈。因此在逻辑表达式中，除了上面提到的“！”外，不允许指向不同数据块的两个指针进行任何操作。
　　可以用 p == \null 来表示指针 p 不指向任何数据，确实不关心 p 的具体指向时，在p不会是悬空指针的情况下，可以用 p != \null 来表示 p 指向某个数据块。
　　一些有两个指针形参p 和q 的函数，调用的两个实参指向不同数据块和指向同一个数据块都能得到各自所要的结果。这种情况是存在的，例如下一章的例4.5。该函数的验证肯定分成两种情况。怎样用断言区别这两种情况呢？若指向同一数据块的要求用断言 p == q 表示，则指向不同数据块的要求用断言 !(p == q) 或 p != q 表示。若指向同一数据块的要求用断言 p == q ± e 表示，则指向不同数据块的要求用断言 !( p == q ± e)（或p != q ± e）表示。
　　基于安全C的定义，指向动态分配的数据块的指针之间只能出现相等与否的断言，或者指针是否等于NULL 的断言。
　　和C语言不同的是，SCSL不会把常数0 隐式转换成指针 \null，也不允许进行这样的强制转换。
　　和C不一样的是，在逻辑表达式中，包括在幽灵代码中，可以出现数组区间表达式和数组区间之间的关系断言。例如，数组区间表达式 a[e1..e2]（a 是数组名或数组元素的指针，e1 必须小于或等于e2 ）和数组区间关系断言 a[e1..e2] <= b[e3..e4]（e4-e3 必须等于e2-e1）。若 e3= e1+n，则后者表示 \forall integer i:[ e1..e2].a[i] <= b[i+n]。因此数组区间之间的关系断言实际上是对应全称量化断言的一种简洁表示。即使a 和b 是同类型的程序数组，也不允许用 a == b 来表示它们的对应元素相等，因为在C语言中数组名是指向数组第一个元素的指针，若允许则断言 a == b 可能有歧义。为避免歧义，表示程序数组a 和b 对应元素相等时，两边都必须用区间表达式，例如断言 a[0..99] == b[0..99]，其中a 和b 的长度都是100。对于程序数组，断言 a == b 表示两个指针相等。有关逻辑数组在第7章介绍。在幽灵代码中，数组还可以区间赋值。有关幽灵变量和语句在第9章介绍。

　　对于一般的数组和指针，有2个内建函数。

1. 长度函数 integer \length(τ p)：
   这是一个多态函数，τ可以是任意的数组类型或任意的指针类型。\length(τ p) 表示有效指针p 所指向的一片τ 类型元素构成的数据区间中τ 类型元素的个数。注意，在C语言中，单独的数组名是指针类型。
2. 偏移函数 integer \offset(τ p)：
   与上述函数一样，它是一个多态函数。其结果是有效指针p 所指向的元素在这片区间中的偏移（以一个元素所占区间大小为单位），0 <= \offset(p) < \length(p)。

// 例3.9
#define MAX_LEN 10000
/*@	requires \length(a) == m && 0 < m <= MAX_LEN && \offset(a) == 0;
	assigns a[0..m-1];
	ensures \length(a) == m && 0 < m <= MAX_LEN && \offset(a) == 0 
					     && \forall integer i:[0..m-2]. a[i] <= a[i+1];
*/
void bubbleSort(int *const a, int const m) {
	int low, up, j, k, temp;
	low = 0; up = m-1; k = up; 

	/*@ loop invariant 
		\length(a) == m && 0 < m <= MAX_LEN && \offset(a) == 0 && low == 0 && up == m-1 
	   && (   k == up && (\forall integer i:[k+1..up-1].a[i] <= a[i+1])	
	          ||
		    low <= k < up && 
		    (\forall integer i:[low..k].a[i] <= a[k+1]) && (\forall integer i:[k+1..up-1].a[i] <= a[i+1])
		);
	*/
	while( k != low) {
		j = low;
		/*@ loop invariant 
			\length(a) == m && 0 < m <= MAX_LEN && \offset(a) == 0 &&
			low == 0 && up == m-1 && k != low && low <= j <= k &&
			(  k == up && (\forall integer i:[low..j-1]. a[i]<=a[j]) &&
				    (\forall integer i:[k+1..up-1].a[i]<=a[i+1])			||
			   low < k < up && (\forall integer i:[low..j-1].a[i] <= a[j]) &&
			           (\forall integer i:[low..k].a[i] <= a[k+1]) && (\forall integer i:[k+1..up-1].a[i ]<= a[i+1])
			);
		*/
		while( j != k ) {
			if (a[j] > a[j+1]) {
				temp = a[j]; a[j] = a[j+1]; a[j+1] = temp;
			}
			j = j + 1;
		}
		k = k -1;
	}
}
									图3.6冒泡排序函数

// 例3.10
int f(int x);
int g(int x);
…
//@ requires p == &f || p == &g;
void h(int(*p)(int)) { …}

  图3.7 使用函数指针的一个简单例子

　　C聚集类型的对象（结构体、共用体和数组）可以在逻辑表达式中作为项的值。它们可以作为参数传递给逻辑谓词和逻辑函数，也可以从逻辑函数返回，除了共用体外，其余的也可以进行相等与否比较等。3.6节已经提到，数组名作为项时在逻辑表达式和幽灵代码中代表整个数组。
　　在逻辑表达式中，对于一个共用体u 来说，在任何情况下，不能出现有关 u.a 的断言和 u.b 的断言的合取，因为共用体的不同成员a 和b 不会同时存在。若出现这样的情况，则该合取式为 \false。
　　对于C代码中已定义的聚集类型，可以声明这些类型的逻辑变量，它们可用来表达函数出口聚集类型的对象与其在函数入口的值的变化。

　　C语言虽然没有字符串类型，但有一些与字符串相关的内容。

• 有字符串常量。例如 "abc" 和 "123"，其中的字符不能是'\0'。
• 字符指针指向的地址连续的字符序列若出现'\0'，则第一个'\0' 之前的部分构成由这个字符指针指向的字符串。该指针这时可以看成字符串指针。连同其存储特性一起考虑的字符串称为物理字符串。物理字符串的存储特性就是指它以'\0' 作为结束标记。
• 有一些适用于物理字符串的内建函数。

1. 判断字符指针 str 指向的内容是否构成长度为 n 的逻辑字符串的谓词
predicate \is_string(char *str, integer n) =
　　　　　　　　　　n >= 0 && n <= \length(str) - \offset(str) &&
　　　　　　　　　　(\forall integer i:[\offset(str) .. \offset(str)+n-1].^str[i] > 0);
其中 ^str 代表 str 所指向的数据块（若用第7章方式，“^”符号是不需要的），\offset(str) 表示 str 指针在 ^str 数据块中的偏移，即 str == ^str + \offset(str)。由此看出，谓词应用 \is_string(s, m) 的值依赖于实变元的显式描述的一些属性，例子可见4.3节例4.5。
　　若 str 是字符数组的名字，则上面谓词的定义体简化为：

n >= 0 && n <= \length(str) && (\forall integer i:[0 .. n-1]. str[i] > 0)
2. 判断字符指针 str 的内容是否构成长度为 n 的物理字符串的谓词
predicate \is_pstring(char *str, integer n) =
　　　　　　　　\is_string(str, n) && \length(str) - \offset(str) >= n+1 && ^str[\offset(str)+ n] == 0;
显然，\is_pstring(str, n) ==> \is_string(str, n)。


3. 求物理字符串长度的函数 \strlen
　　在断言中，不管是逻辑字符串还是物理字符串都要有长度信息。但是有些代码并不关注物理字符串的长度，它们是依据是否扫描到结束标记来编程的。为了便于把描述物理字符串的断言统一到都有长度变元的形式，引入函数 \strlen。
　　该函数的类型是char* → integer，并且要求其变元必须指向一个物理字符串。
　　按上面所给定的类型，写不出该函数的归纳定义。该函数是一个未解释函数，其含义体现在如下的内建引理中。

lemma pstringProperty:
　　　　　　　　　　\forall char *str. \forall integer n. \is_string(str, n) && ^str[\offset(str)+n] == 0
　　　　　　　　==> \strlen(str) == n;

　　在不关心物理字符串的长度时，程序标注可以用 \is_pstring(str, \strlen(str)) 来表示str 指向一个物理字符串。有了这个函数后，在串长为m 时，把 \is_pstring(str, m) 写成 \is_pstring(str, \strlen(str)) && \strlen(str) == m 也是一样的。


4. 取逻辑字符串的函数（使用条件为 n >= 0）
　　从字符数组取长度为n的逻辑字符串的函数，其类型是：char* × integer → STRING。

logic STRING \string(char *str, integer n) = {^str[\offset(str) .. \offset(str)+n-1], n};

若n 等于0，则该逻辑函数的结果是空串。
　　即该函数的结果是由 ^str[\offset(str)], ^str[\offset(str)+1], …, ^str[\offset(str)+n-1] 构成的长度为 n 的字符串。为方便表达，这里采用第7章所提供的数组区间方式（即 ^str[\offset(str).. \offset(str)+n-1]）来表示逻辑字符串的内容，并用{…, …}方式来表示有两个域的记录的值。这个函数仅在 (\is_string(str, m) || \is_pstring(str, m)) && m >= n 情况下使用。先前介绍说 \string(str, m) 是STRING类型的最简单的非常量的项形式，其实就是把 \string 函数应用的结果作为逻辑字符串的项。
　　为易理解起见，下面介绍关于字符串操作的内建函数时，所列谓词和函数都把字符指针 str、str1 和 str2 等都限定为是数组名的情况。


5. 逻辑字符串之间的关系运算 ==、!=、<、<=、> 和 >=（使用条件为 m >= 0 且 n >= 0）
　　它们的类型都是STRING × STRING → boolean。上面这些关系算符都是中缀算符，结果类型是布尔型，在下面介绍它们的定义时，把它们看成谓词的名字。串并置算符 "+" 也按这种方式描述。
　　（1）相等与否运算 == 和 !=

predicate "==" (STRING \string(str1, m), STRING \string(str2, n)) =
　　　　　　　　　　m == n && (\forall integer i:[0..m-1].str1[i] == str2[i]);

　　这是字符串 \string(str1, m) 和 \string(str2, n) 的相等关系运算，不相等关系可类似地定义。
　　（2）大小关系运算 <, <=, >, >=
　　小于关系的定义如下，其他关系的定义可类似地写出。

predicate boolean "<" (STRING \string(str1, m), STRING \string(str2, n)) =
　　　　\exists integer k:[0..n-1].　　//若n== 0，则结果一定为\false
　　　　((\forall integer i:[0..k-1].str1[i] == str2[i]) &&　　//这两行针对m >= 0, n > 0
　　　　(k >= m || str1[k] < str2[k])); //若k >= m，则n > m且两者前k-1个
　　　　　　　　　　　　　　　　//字符相同，则结果一定为\true



6. 逻辑字符串并置函数 "+"（使用条件为 m >= 0 且 n >= 0）
　　该函数的类型是: STRING × STRING → STRING。

logic STRING "+" (STRING \string(str1, m), STRING \string(str2, n)) =\string(str3, m+n)，

　　其中str3 是新的字符数组，它满足：

if (m == 0 && n == 0) 结果 \string(str3, m+n) 是空串；
else 结果\string(str3, m+n) 满足：str3[0..m-1] == str1[0..m-1] && str3[m..m+n-1] == str2[0..n-1]。



7. 取逻辑字符串前缀的函数 \prefix（使用条件为 m >= 0，n >= 0 且 n <= m）
　　该函数的类型是：STRING × integer → STRING。

logic STRING \prefix(STRING \string(str, m), integer n) = \string(str, n);

　　该函数的结果是str 数组中从第1字符到第n 个字符构成的逻辑字符串。注意，若 n == 0，则结果是空串。


8. 取逻辑字符串后缀的函数 \suffix（使用条件为 m >= 0，n >= 0 且 n <= m）
　　该函数的类型是：STRING × integer → STRING。

logic STRING \suffix(STRING \string(str, m), integer n) = \string(str+(m-n), n); (= str[m-n..m-1])

　　该函数的结果是str 数组中从第m-n+1 字符开始到第m 个字符，共n 个字符构成的逻辑字符串。注意，若n 等于0，则结果是空串。


9. 一个字符是否属于某个逻辑字符串的谓词 \membership（使用条件为m >= 0）
　　该谓词的类型是：STRING × char → boolean，它只用于有长度信息的逻辑字符串。

inductive \membership(STRING \string(str, m), char c) =
　　　　　　　　　　m == 0 ? \false
　　　　　　　　　　　　　 :　m >= 1 && str[0] == c ? \true : \membership(\string(str, m-1), c);



10. 逻辑字符串str1 是否包含str2 的谓词 \contains（使用条件为 m >= 0 且 n >= 0）
　　该归纳谓词的类型是：STRING × STRING → boolean

inductive \contains(STRING \string(str1, m), STRING \string(str2, n)) =
　　　　　　　　　　m < n ? \false
　　　　　　　　　　　　　: \prefix(\string(str1, m), n) == \string(str2, n)
　　　　　　　　　　　　　　? \true
　　　　　　　　　　　　　　: \contains(\string(str1+1, m-1), \string(str2, n));



11. 计算str2 首次出现在str1 中的索引的函数 \index（使用条件为 m >= 0 且 n >= 0）
　　该归纳谓词的类型是：STRING × STRING → long

logic long \index(STRING \string(str1, m), STRING \string(str2, n)) =
　　　　　　　　　　m < n ? n-1
　　　　　　　　　　　　　: \prefix(\string(str1, m), n) == \string(str2, n)
　　　　　　　　　　　　　　? 0
　　　　　　　　　　　　　　: 1+ \index(\string(str1+1, m-1), \string(str2, n))

　　该函数的结果若在区间 [0..m-n] 之间，则是逻辑字符串str2 首次出现在str1 中的索引，否则结果大于等于m，表示逻辑字符串str2 并未出现在str1 中。


12. 取逻辑字符串中第n 个字符的函数 \char（使用条件为 m >= n > 0）
　　该函数的类型是：STRING × long → char。

logic char \char(STRING \string(str, m), long n) = str[n-1]

　　对于上述这些内建函数，在C语言的标准库中有功能类似的函数，但是它们都是操作于物理字符串，出现在程序中。这里的逻辑函数和谓词是出现在断言中的。

// 例3.11
// 库函数strcpy(char* dest, const char* src)的验证，这个协议适用于dest 和src 指向不同的数据块
//@	logic char *olddest, *oldsrc; logic integer m;
/*@	requires \is_pstring(src, m) && \length(dest) - \offset(dest) > m && olddest == dest && oldsrc == src;
	ensures \result == olddest && \is_pstring(\result, m) && \is_pstring(oldsrc, m) && 
		\string(\result, m) == \string(oldsrc, m);
*/
char * strcpy(char * dest, const char * src);

//@	logic integer m, n; logic char *olddest, *oldsrc;
/*@	requires \is_pstring(dest, m) && \is_pstring(src, n) && m + n < \length(dest) - \offset(dest) &&
		olddest == dest && oldsrc == src;
	ensures \is_pstring(\result, m+n) && \is_pstring(oldsrc, n) && \result == olddest &&
		\string(\result, m+n) == \string(olddest, m)) + \string(oldsrc, n);
*/
char * strcat(char* dest, const char* src);

					图3.8 库函数strcpy 函数和strcat 函数的协议

// 例3.12
char* p = "abc";
main() {
char* q;
char* t = "abc"; q = "abc";
… …
}
图3.9 字符串常量的一个例子

　　函数协议（function contract）是指函数定义和函数使用之间的约定，函数协议的文法见图4.1。从文法上看，函数协议允许出现在C 声明可出现的地方，但实际限定它们必须出现在相应函数的声明或定义之前。尤其是，若函数f 的应用和定义分处不同源文件时，f 的所有协议必须分别出现在 f 的各个声明之前，f 的所有声明应该在这些源文件都包含的头文件中。

4.1 内建构造 \result 和 \old

4.2 简化的函数协议

4.3 带命名行为的函数协议

4.4 异常终止

4.5 多协议

4.6 缺省协议和函数指针变量的协议

4.7 main函数的前条件

4.8 对形参有void*类型的函数协议的特别要求

　　函数的后条件（ensures子句）经常要引用函数的结果，还有可能引用函数形参和所操作的全局变量在函数初始状态下的值。

1. \result 指称函数的返回值。
   \result 只能出现在返回类型不是 void 的函数的ensures 子句中。
2. 内建构造 \old(t) 用来记住全局变量 t 或者函数形参 t 所对应的实参在函数入口点的值。
   例如，在一般情况下，函数入口有 \old(x) == x，其中 x 是函数的形参。该断言用于验证与 x 对应的实参在函数调用前后的值的变化。内建构造 \old(t) 可理解为一个多态函数，其中 t 是代表程序变量的左值的简单表达式。简单表达式是指没有赋值运算符，也不以函数调用、条件表达式或逗号表达式作为其子表达式的表达式。例如变量 m、a[0]、r.b 和 p->next 等。

• 带 \old 的断言 \old(b+c) == b+c 不被接受，因为 \old(b+c) 中的 b+c 不是左值表达式。需要的话，应该写成 \old(b) + \old(c) == b + c。类似地，断言
  \old(\forall int i:[0..99]. a[i] == 0) == \forall int i:[0..99]. a[i] == 0
  
  也不被接受，因为\old 构造的变元是断言。需要的话，应写成
  
  \forall int i:[0..99]. \old(a[i]) == a[i]
• 若函数前条件的 \old(t) == t 的 t 中含有可以改变 t 左值的变量，例如 \old(a[x]) 和 \old(head->(next:m)->data) 中的 a、x、head、m 和 head->(next:m) 的程序变量或幽灵变量，则在该函数中不能对这些变量赋值，因为赋值之后 t 的左值可能就不再等于函数入口处 t 的左值。
注意，若函数前条件中有断言
\forall int i:[0..99]. \old(a[i]) == a[i]，
\old(a[i]) 中虽有 i，但 i 是可以在0到99之间变化的该全称量化断言的约束变元。i 值的变化虽然改变 a[i] 的左值，但该左值总表示 a[0] 到 a[99] 这100个数组元素中某个数组元素的左值。因此这不是对 i 赋值，i 不属于上面所说的不能赋值的变量。类似的情况见例7.3，例7.3的函数前条件中有
\forall int i:[0..m-1].\old(head->(next:i)->data) == head->(next:i)->data
同样，其中 i 是全称量化断言的约束变元，i 的值变化，则 head->(next:i)->data 的左值就变化。只要 i 的值在 0 到 m-1 之间，head->(next:i)->data 的左值就是该链表上某个表元的 data 域的地址。
　　在 \old(t) 中，t 的内部无需也不允许存在外加 \old 的子项，也就是 \old 构造不必也不能嵌套使用。

3. 在一些特殊场合，会有 \old(dest[i+k]) == dest[i] 或者 \old(dest[i]) == dest[i+k] 这样的需求。
例如，在例4.5中，在函数协议的一种命名行为中（命名行为的含义见4.3节），前条件和后条件中分别有
\forall integer i:[m-k..m].olddest[i] == \old(olddest[i]) 和
\forall integer i:[0..m-k-1].olddest[i] == \old(olddest[i+k])

• 在函数前条件中，仍然必须是 \old(t) == t；
• 而在循环不变式、程序点断言和函数后条件中，可以是 \old(t) == t ± e 或者 \old(t ± e) == t。其中 e 只允许是简单表达式，并且 e 中没有程序可赋值的变量。

4. 另外，t 可以是代表数组区间的项，例如 \old(id[0..al]) == id[0..al]。对于这里的上下界表达式，也可以有符合第3点中要求的 ± e 表达式。

• 若 x 是全局变量或形参，并且被 const 修饰，则没有必要用 \old(x) 来记住 t 在函数入口处的值，因为 x 在函数的执行过程中不会被改变，x 可直接出现在函数后条件中。
• 若 x 是指针类型的全局变量或形参，其指向的数据没有 const 修饰，情况与上一点就不一样了。若想验证函数执行前后，相应实参指向数据的变化，这时可以用 \old 构造来记住指针 x 在函数入口点所指向数据的值。例4.5是使用 \old 构造的一个例子，后面各章还有一些例子。
• 一般情况下 t 是左值表达式，唯一的例外是，t 可以是并非左值的STRING类型的最简单的非常量项 \string(t1, t2)，其中 t1 和 t2 是不带函数调用的简单项。若要仔细推敲，t1 是 \string(t1, t2) 的左值。
• 函数前条件有某个 \old(…) 时，函数其它地方的标注才可以出现这个 \old(…)。包括上面第3和第4点提到的略有区别的情况。
  　　按照 \old 构造的定义，在函数入口点，断言 \old(t) == t 一定成立。在函数前条件中添加断言 \old(t) == t，是在其他程序点验证 t 的当前值和 t 在函数入口点的值之间的关系的基础，尤其是 t 涉及到通过指针可访问一批数据时，用这种方式比较方便。例如，链表插入函数使得结果链表和参数链表之间的区别仅是前者在某个位置多了一个节点及其数据，见例7.3。
  　　后面还会介绍，存在其他方式可用来表达相同或类似的需求。
• 可用逻辑变量记住t 在函数入口状态下的值，逻辑变量的介绍见7.2节。例子可见例3.11，还可见例7.1和例7.2等。采用逻辑变量的方式比采用 \old 构造的方式简单，因此，\old(t) 一般用于t 中有易变数据结构的节点指针类型的变量的情况。两种表示方式的区别与联系请见7.2节。

　　一个简单的函数协议 只有简单子句，没有命名行为，其形式如下：

1. 函数的调用者必须保证，其调用状态使得性质 P₁ && … && P_m 成立。P₁ && … && P_m 即常说的函数前条件（在介绍带命名行为的协议后还会充实）。
   就程序变量而言，只有形参和全局变量以及由它们开始的访问路径所达的变量可以出现在 P_i(1 ≤ i ≤ m)中。对于指针类型的形参和全局变量，调用者必须保证指针型的实参和全局变量相互之间不会形成别名，除非这种别名是从函数前条件可以推导的。
2. 被调用函数必须保证，其返回状态使得性质 Q₁ && … && Q_k 成立，Q₁ && … && Q_k 即常说的函数后条件。
   就程序变量而言，局部变量和未带 const 修饰符的形参不能出现在 Q_i (1 ≤ i ≤ k) 中。
   函数前后条件中可以出现第7章介绍的逻辑变量，也可以出现第9章介绍的幽灵形参和幽灵全局变量。
3. V₁, …, V_n 是指可能被函数赋值的非局部变量。
   它分成两种情况，一种是属于可赋值的外部变量（包括由可访问外部变量开始的访问路径所代表的变量，因而有可能是堆变量），另一种是属于通过指针型形参开始的访问路径所代表的可赋值变量。下面分别介绍。对于堆指针指向的易变数据结构，存在一些特殊性，在下面（1）和（2）之后单独介绍。

• 若 f 函数仅能被本文件的函数调用，f 修改的静态外部变量和外部变量列在同一个 assigns 子句中。
• 若 f 函数仅能被其它文件的函数 g 调用，则 f 的协议必须出现在f 所在源文件和g 所在源文件共享的某个头文件中。但是，f 函数修改的静态外部变量不必列在 f 函数协议的 assigns 子句中。因为 g 函数协议上根本不会出现 f 函数所修改的静态外部变量。
• 若 f 函数能被本文件的函数调用，也能被其它文件的函数 g 调用，则 f 的协议也必须出现在 f 所在源文件和 g 所在源文件共享的某个头文件中。这时f 函数的 assigns 子句需要区分修改的外部变量和静态外部变量，其中静态外部变量列在 static assigns 之后。例如：
  assigns v1, v2;　　　// v1和v2是外部变量。
  static assigns x;　　　// x是静态外部变量。

• 所说的访问路径都由变量标识符（包括幽灵变量，也包括逻辑变量）和数组名开始。在此谈论访问路径时，把访问路径 *p… 和 &b… 视同为 p*… 和 b&…，即都视为由变量标识符开始的访问路径，以简化描述，同时也表明 *p… 和 &b… 不包括单独的 p 和 b。
• 所说的访问路径包括像 a[e] 和 a[e1..e2] 这样代表一个数组元素 a[e] 和数组元素集 {a[e1], …, a[e2]} 的访问路径。若访问路径中的指针 a 会被赋值，而仍希望 a[e] 等的 a 表示 a 在函数入口的初值的话，则需要使用 \old(a) 描述，例如 \old(a)[e]。这里的 e、e1 和 e2 只能是简单表达式，其中若有变量 x，则 x 应是外部变量。若使用的是 \old(x)，则 x 在本函数协议的 S 集合中，否则 x 不在该 S 集合中。

• 一般情况下，V_i 一定不会是单纯的指针型形参，因为对形参赋值不会改变对应的实参。当Vi是有效指针时，它一定代表指针型形参指向的对象（*V_i 或 V_i -> next等），并且形参声明中是允许对指向对象赋值的。
  特殊情况指 V_i 是堆指针，并且 V_i 指向的对象会在代码中被 free(V_i) 释放，导致对应实参变成悬空指针。把这种情况留到稍后专门解释堆指针时介绍。
• 对 V_i 赋值修改的是什么变量，由调用的实参决定的。虽然实参可能不是可访问的外部变量，但也肯定不是该函数的局部变量，因此 V_i 也属于上面所讨论的 S 集合。函数前后条件中对这类形参的描述，实际上就是对实参的描述。
• 若 V_i 是上面所提到的 a[e] 和 a[e1..e2] 这样的形式，并且a 是形参，若可以对 a 赋值，而仍希望 a[e] 等的 a 表示 a 在函数入口的初值的话，则需要使用 \old(a) 描述，例如 \old(a)[e]，以保证都是用 a 在函数入口的值来计算下标变量的地址。若 e、e1 和 e2 中有变量 x，则一般使用的都是 \old(x)，否则 x 不在本函数协议的S集合中。

• 掌握函数调用之前程序点的哪些断言不受调用的影响，可以延续到调用点之后的程序点。
• 以文件为单位的分模块验证。

/*@ requires x >= 0;
    ensures  \result >= 0;
    ensures  \result * \result <= x;
    ensures  x < (\result + 1) * (\result + 1);
*/
int isqrt(const int x);

/*@ requires x >= 0 && \old(x) == x;
    ensures  \result >= 0;
    ensures  \result * \result <= \old(x);
    ensures  \old(x) < (\result + 1) * (\result + 1);
*/

#define MAX_VALUE 1000
/*@ requires p != \null && \old(*p) == *p && *p < MAX_VALUE;
    assigns  *p;
    ensures  *p == \old(*p) + 1;
*/
void incrstar( int * const p) {
    *p = *p + 1;
}

#define MAX_VALUE 1000
//@ logic int oldValue;
/*@ requires p != \null && oldValue == *p && *p < MAX_VALUE;
    assigns  *p;
    ensures  *p == oldValue + 1;
*/
void incrstar( int * const p) {
    *p = *p + 1;
}

int a=0, b=0, c=0;
//@ requires c == 0; assigns c; ensures c == 1;
void f2() { c = c + 1; }
//@ requires b == 0 && c == 0; assigns b,c; ensures b == 1 && c == 1;
void f1() { f2(); b = b + 1; }
//@ requires a == 0 && b == 0 && c == 0; 
//@ assigns a, b, c; 
//@ ensures a == 1 && b == 1 && c == 1;
void test() { f1(); a = a + 1;}

• 文件d.h：

extern int b, c;
//@ requires b == 0 && c == 0;  assigns b, c;  ensures b == 1 && c == 1;
void f1();

• 文件file1.c：

include “d.h”
int a;
//@ requires a == 0 && b == 0 && c == 0; 
//@ assigns a, b, c; 
//@ ensures a == 1 && b == 1 && c == 1;
void main() { f1(); a = a + 1; }

• 文件file2.c：

include “d.h”
int b, c;
//@ requires c == 0;  assigns c;  ensures c == 1;
void f2() { c = c + 1; }
void f1() { f2(); b = b + 1; }          // 函数f1的协议在头文件d.h中。

　　函数协议的一般形式 可以包含若干命名行为，这些行为的名字必须有区别。下面一般都用2个命名行为来解释。例如：

• 若x 在函数中有可能被赋值，则必须写成 \old(x)，以表示 assumes 子句用的是 x 在函数入口处的值，通常用的是断言 \old(x) == x。
• 若代码中有不允许函数对 x 赋值的修饰，则在 assumes 子句可直接写 x。

1. P 是任何调用都应满足的前条件。任何满足 P 的调用在调用点后能得到性质 Q。
2. A₁ && R₁ 和 A₂ && R₂ 分别是某些额外性质。若调用满足 P 以外，还满足 A_i && R_i（1 ≤ i ≤ 2），则在调用点后除了得到 Q 以外，还能得到 Q₁ 和/或 Q₂。
3. A_i && R_i（1 ≤ i ≤ 2）还有这样的特点，若A_i 为真则R_i 为真，即 A_i ==> R_i。这是把A_i 单独列在 assumes 子句的原因。

1. 函数的调用者必须保证，其调用状态使得性质 P && (A₁ ==> R₁) && (A₂ ==> R₂) 成立。
2. 被调用函数必须保证，其返回状态使得性质 Q && (A₁ ==> Q₁) && (A₂ ==> Q₂) 成立，也就是使得函数后条件成立。
3. 对于 i = 1, 2，若调用者的调用状态能使 A_i 成立，则列在 V_j（j ≠ i）而未列在 V_i 中的全局变量和以其名字开头的左值表达式所表示的变量，在调用之后的状态中保持不变。
4. 带命名行为的协议相当于把函数前后条件分成了若干种命名情况，改进可读性。
5. 命名行为中的 assumes 子句缺省时也默认为 \true。

// 例4.5　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
//早年的串拷贝库函数strcpy(char* dest, char* src)的验证
// 这个协议适用于dest和src指向不同的数据块和指向同一个数据块两种情况
//@ logic char *olddest, *oldsrc; logic int m, k;
/*@
requires \offset(dest)==0 && \length(dest) > 1 && olddest==dest && \old(dest) == dest 
	&& oldsrc==src && \offset(src)>=0 && \length(src)>1 
	&& \old(olddest[0..\length(olddest)-1])==olddest[0..\length(olddest)-1];
assigns \old(dest)[0..\length(\old(dest)) -1];
ensures \result == olddest;
    behavior non_overlap:
        assumes !(oldsrc == olddest+k);	//根据SCSL手册3.7节，可知oldsrc和olddest指向不同的数据块。
        requires \is_pstring(src, m) && \length(dest) > m ;
        ensures \is_pstring(\result, m) && \is_pstring(oldsrc, m) && \string(\result, m) == \string(oldsrc, m);
    behavior overlap:
        assumes oldsrc == olddest+k;
        requires \is_pstring(dest, m) && 0 <= k <= m && \is_pstring(src, m-k) && src == dest + k  ;
        ensures \is_pstring(olddest, m-k) && 0 <= k <= m && 
			(\forall int i:[0..m-k].olddest[i] == \old(olddest[i+k])) &&
			olddest[m-k+1..\length(olddest)-1] == \old(olddest[m-k+1..\length(olddest)-1]);
    complete behaviors;
    disjoint behaviors;
*/
char* strcpyOld(char* dest, char* src){
	char* p;
	//@ ghost int n;
	p = dest;
	*dest = *src;
	//@ ghost n = 0;
	/*@ loop invariant
		!(oldsrc == olddest + k) && 0 <= n <= m && dest == olddest + n && src == oldsrc + n 
		&& p == olddest && \old(dest) == olddest && \offset(olddest) == 0 
		&& \is_string(olddest, n) && \string(olddest, n) == \string(oldsrc, n) 
		&& olddest[n+1..\length(olddest)-1] == \old(olddest[n+1..\length(olddest)-1]) 
		&& \is_pstring(oldsrc, m) && \length(olddest) > m && *dest == *src 
		||
		src == dest + k && 0 <= k <= m && 0 <= n <= m-k && dest == olddest + n 
		&& p == olddest && \is_pstring(src, m-k-n) && oldsrc == olddest + k && \old(dest)==olddest 
		&& (\forall int i:[0..n].olddest[i] == \old(olddest[i+k])) 
		&& (\forall int i:[n+1..\length(olddest)-1].olddest[i] == \old(olddest[i])) 
		&& (*src != 0 && \is_pstring(olddest, m) && n < m-k ||
			*src == 0 && \is_pstring(olddest, m-k) && n == m - k) 
		&& \offset(olddest) == 0;
	*/
	while(*src != 0){
		dest = dest + 1;
		src = src + 1;
		*dest = *src;
		//@ ghost n = n + 1;
	}
	return p;
}
							 图4.2 早年的库函数strcpy的协议

// 例4.6
/*@	
	behavior p_changed:
		assumes n > 0;
		requires p != \null;
		assigns *p;
		ensures *p == n;

	behavior q_changed:
		assumes n <= 0;
		requires q != \null;
		assigns *q;
		ensures *q == n;
*/
void f(const int n, int* const p, int* const q) {
	if (n > 0) *p = n; else *q = n; 
}	

		图4.3 命名行为各带assigns子句

　　函数协议的 ensures 子句并没有包括对函数异常终止状态（调用 exit 之后的状态）的约束。因此对于有 exit 调用的函数，函数协议中必须包括 exits 子句；若无 exit 调用，则无须包括 exits 子句。若 exits 子句有堆指针断言，则这部分断言只能是8.3.1节提到的简单指针断言或者 \dangling(p)，其中 p 是堆指针。

　　例4.7 在图4.4中，前一部分是库函数 exit 的规范。在 ensures 子句中，它什么也不保证。在 exits 子句中，\exit_status 是内建的整型变量，该子句给出的异常标识就是调用 exit 函数的实参。
　　图4.4的其余部分是可能调用 exit 函数的 mayExit 函数及其规范，位于其前面的 status 是全局变量。mayExit 函数的异常终止 exits 子句告知出现异常的原因以及调用 exit 函数所用的参数等。
　　图4.4中的函数 mayExit 的协议并不完备，因为该协议允许在不执行 exit 时也修改变量 status。使用命名行为，可以区分正常和异常情况，mayExit 函数的相应规范见图4.5。

// 例4.7
int status = 0;
/*@	ensures	\false;
	exits	\exit_status == status;
*/
void exit(const int status);

/*@	assigns status;
	exits cond == 0 && \exit_status == 1 && status == val;
*/
void mayExit(const int cond, const int val) {
	if(cond == 0) {status = val; exit(1);}
}
		图4.4 异常终止的一个例子

// 例4.7
int status = 0;
/*@	behavior no_exit:
		assumes cond != 0;
		ensures \false;

	behavior no_return:
		assumes cond == 0;
		assigns status;
		exits \exit_status == 1 && status == val;
		ensures \false;
*/
void mayExit(const int cond, const int val);

		图4.5 异常终止的另一个例子

　　C的函数仅能定义一次但可以声明多次。可以对函数的每个声明标注一个协议。这时把这个函数看成是有多个协议的函数。协议有多个命名行为的函数不能称为多协议函数，它们不是一回事。
　　在多协议的情况下，若调用点的状态满足其中部分协议，则调用之后的状态满足这一部分协议的后条件。
　　对于有完备且两两不相交性质的n 个命名行为的函数协议，可以拆成n 个函数协议，相互正交的性质分别属不同的协议。这时最多只有一个协议能得到验证。

　　例4.8 图4.6是树堆（treap）中两个协议的右旋函数。树堆是一种有额外性质的BST（二叉排序树），BST 在《安全C语言使用手册》第2章中已经介绍，在本手册的后面也会用到。BST 的各个节点增加一个随机附加域使得它还满足堆（见例5.2）的性质，就构成这里定义的树堆。
　　下面先介绍图4.6的代码用到的二叉树节点的数据类型。

typedef struct node {	// 其中 priority 域就是随机附加域。
    int data; int priority; struct node* l; struct node* r;
}Node;
//@ shape l, r : binary_tree;

 // 例4.8 面向树堆的有两个协议的右旋函数（部分）
//@ logic Node* oldt; logic integer x, y, z; 
/*@
    requires    // 这个协议用于插入函数，在插入左子树后可能出现的右旋。
        oldt == t && BST(t) && gt(y, t) && lt(z, t) && x <= t->priority && heap_tree(t->l) &&
        heap_tree(t->r) && priority_le(t->priority, t->r) && t->l->priority < t->priority &&
        priority_le(t->priority, t->l->l) && priority_le(t->priority, t->l->r);
    assigns *t;
    ensures
        oldt == \result->r && BST(\result) && gt(y, \result) && lt(z, \result) &&
        heap_tree(\result) && priority_le(x, \result->l) && priority_le(x, \result->r)
        ;
*/
Node* rRotate(Node* t);

/*@
    requires    // 这个协议用于删除函数，在删除左子树后可能出现的右旋。
        t != \null && t->l != \null && oldt == t && BST(t) && gt(y, t) && lt(z, t) && heap_tree(t->l) &&
        heap_tree(t->r) && priority_le(x, t->l) && priority_le(x, t->r) && t->l->priority < t->r->priority;
    assigns *t;
    ensures
        \result != \null && \result->r != \null && oldt == \result->r && BST(\result) && gt(y, \result) &&
        lt(z, \result) && priority_le(\result->priority, \result->l) && 
        priority_le(\result->priority, \result->r->l) &&
        priority_le(\result->priority, \result->r->r) && x <= \result->priority && priority_le(x,\result->l) &&
        priority_le(x,\result->r->l) && priority_le(x,\result->r->r) && heap_tree(\result->l) &&
        heap_tree(\result->r->l) && heap_tree(\result->r->r)
        ;
*/
Node* rRotate(Node* t){
    // 对以*t为根的树作右旋处理，处理之后t指向新的树根节点，它是原来的左子树根节点
    Node* lc;	
    lc = t->l;   t->l = lc->r;  lc->r = t;  t = lc;    return t;
}

						图4.6 面向树堆的有两个协议的右旋函数

　　先前已经提到，函数可以有缺少某些子句的协议。例如，requires 子句和 ensures 子句缺省时都看成 \true。
　　也可以没有为函数书写协议，这表示该函数协议中的 requires、assigns 和 ensures 都使用默认情况，而不是该函数没有协议。
　　对于函数指针变量，在它们的声明处，无需用标注给出它们的协议，因为这时尚不知它们代表哪个函数。

　　main 函数执行的初始状态，不仅包括了它所在C源文件确定的外部变量、静态外部变量和静态局部变量的初值，也包括了将和该文件一起连接的其它C源文件所确定的这三类变量的初值。这些文件中的这三类变量，若在声明时置初值的话，则都是在程序执行之前就静态确定的，它们出现在调用main 函数时的程序状态中是合理的。
　　同其他函数一样，main 函数的前条件按理应由程序员提供，程序员必须把与验证 main 函数有关的初值断言列在 main 函数的前条件中，程序员还要关注 main 函数可能有的形参 int argc 和 char* argv[]。
　　main 函数有形参 argc 和 argv 时，main 函数的前条件就自动有下面的断言：

　　若函数 f 有形参 void* x，则调用 f 时，对应形参 x 的实参必须是具体类型的指针而不是 void 类型的指针。为确保这一点，函数的前条件中必须有对 *x 对应实参类型限定的断言。可参看例4.9（图4.7）中的函数 comp_int 和 comp_str 的协议。图3.2 的断言文法中的断言 \typeof(C-expr) == C-type-name 是一个特殊的内建断言，\typeof(C-expr) 是获取C表达式 C-expr 的类型，C-type-name 是C程序中定义的类型名。
　　在函数 f 中，形参 x 必须先强制成具体类型的指针后才能使用，该具体类型必须和函数前条件中对 *x 的类型限定一致。并且 x 的类型被强制后，不得再次把它强制成其它类型。
　　再看例4.9（图4.7）中对快速排序库函数 qsort 的调用。qsort 的函数原型如下：

/*@ 
    // 这是 qsort 第4个形参（函数指针）的协议（只列出与这里的介绍相关的断言）。
    // 它是 qsort 协议前条件的一部分。
    requires \typeof(*q) == int && \typeof(*t) == int;
    ensures \result < 0 ==> *q < *t || \result == 0 ==> *q == *t 
                                    || \result > 0 ==> *q > *t;
*/

/*@ //这是 qsort 的协议，前条件中有关第4个形参应有的性质见上面的协议
    requires \typeof(*p) == int && \length(p) == len && size == sizeof(int);
    ensures \forall integer j:[0..len-2]. p[j] < p[j+1];
*/

/*@ //同样，这是qsort 第4个形参（函数指针）的协议。
    requires \typeof(*q) == char && \typeof(*t) == char && \is_pstring(q, \strlen(q)) 
	    && \is_pstring(t, \strlen(t));
    ensures \is_pstring(q,\strlen(q)) && \is_pstring(t,\strlen(t)) &&
            ( \string(q, \strlen(q)) < \string(t, \strlen(t)) && \result < 0 ||
              \string(q, \strlen(q)) == \string(t, \strlen(t)) && \result == 0 ||
              \string(q, \strlen(q)) > \string(t, \strlen(t)) && \result > 0 
            );
*/

/*@ //同样，这是qsort 的协议，有关第4个形参应有的性质见上面的协议
    requires \typeof(**p) == char && \length(p) == len && size == 6 * sizeof(char) &&
            (\forall integer j:[0..len-1]. \is_pstring(p[j],\strlen(p[j])));
    ensures (\forall integer j:[0..len-1]. \is_pstring(p[j],\strlen(p[j]))) &&
	     \forall integer j:[0..len-2].
		 \string(p[j], \strlen(p[j])) < \string(p[j+1], \strlen(p[j+1]));
*/

// 例4.9　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
// 整数大小比较函数，作为main函数中第一个qsort调用的最后一个实参。
/*@ requires \typeof(*a) == int && \typeof(*b) == int 
		    && 0 <= \offset(a) < \length(a) && 0 <=\offset(b) < \length(b);
	ensures \typeof(*a) == int && \typeof(*b) == int 
		    && 0 <= \offset(a) < \length(a) && 0 <= \offset(b) < \length(b) 
		    && (\result < 0 && *a < *b || \result == 0 && *a == *b || \result > 0 && *a > *b);
*/
int comp_int(const void* const a, const void* const b){
	int *pa, *pb;
	pa = (int*)a;	 pb = (int*)b;   // 从函数的前条件知道，这两个强制是正确的。
	if (*pa < *pb){ return -1; } if (*pa > *pb){ return 1; } return 0;
}
// 字符串的词典序比较函数，作为main函数中第二个qsort调用的最后一个实参。
/*@ requires \typeof(*p1) == char && \typeof(*p2) == char 
			&& \is_pstring(p1, \strlen(p1)) && \is_pstring(p2, \strlen(p2));
	ensures \typeof(*p1) == char && \typeof(*p2) == char 
			&& \is_pstring(p1,\strlen(p1)) && \is_pstring(p2,\strlen(p2)) 
			&& (\string(p1, \strlen(p1)) < \string(p2, \strlen(p2)) && \result < 0 
				|| \string(p1, \strlen(p1)) == \string(p2, \strlen(p2)) && \result == 0
				|| \string(p1, \strlen(p1)) > \string(p2, \strlen(p2)) && \result > 0);
*/
int comp_str(const void* const p1, const void* const p2){
	char *src, *des;
	src = (char*)p1; des = (char*)p2;
	return strcmp(src, des);
}
/*@ requires \true;  ensures  \result == 0; */
int main(void){
	int i;
	int  a[10] = {3,5,1,8,6,7,2,9,4,0};
	char s[5][6] = {"1235","54321","23451","54322","12344"};
	// 一维整型数组排序
	// 从第4个实参comp_int函数的前条件可以知道，comp_int函数的实参实际是int*类型。
	// 这样，第3个实参sizeof(int)符合要求，实参a的类型也符合要求。
	qsort(a, 10, sizeof(int), comp_int);   
	printf("\n after sorting:\n");
	/*@ loop invariant  0 <= i <= 10 && (\forall int j:[0..8]. a[j] <= a[j+1]) 
			&& (\forall int j:[0..4]. \is_pstring(s[j],\strlen(s[j]))) 
			&& \string(s[0], 4) == "1235" && \string(s[1], 5) == "54321" 
			&& \string(s[2], 5) == "23451" && \string(s[3], 5) == "54322" 
			&& \string(s[4], 5) == "12344"; 
	*/
	for(i=0;i<10;i++){ printf("%d\t",a[i]); }
	// 字符串数组排序	
	qsort(s, 5, sizeof(s[0]), comp_str);    // 类似上面的情况。
	printf("\n after sorting:\n");
	/*@ loop invariant 
			0 <= i <= 5 
			&& (\forall int j:[0..4]. \is_pstring(s[j],\strlen(s[j]))) 
			&& \forall int j:[0..3].
				\string(s[j], \strlen(s[j])) <= \string(s[j+1], \strlen(s[j+1]));
	*/
	for(i=0;i<5;i++){printf("%s\t",s[i]);} return 0;
}
								图4.7 快速排序程序

• 若函数 f 有 void* 类型的形参 x，则函数 f 的协议必须指明x 对应实参的所有可能类型。
  若函数 f 的形参 void* x 所对应实参不是唯一类型的，例如前条件中有 (\typeof(*x) == char || \typeof(*x)== short || \typeof(*x)== long)。则一般来说，这时函数 f 的代码需要根据 *x 的类型来分情况处理。由于 \typeof(*x) 是不能用到代码中来指示分情况处理的，因此函数f 还需要有另一个形参 y 来帮助实现这一点，并且在函数前条件中把 y 和 \typeof(*x) 取值的对应用断言表达清楚。
• 同样，若函数 g 的形参中有作为形参的函数 f_形，则 f_形 的协议必须指明其 void* 类型形参对应实参的所有可能类型。
  并且对函数g 采用多协议方式方式来描述，每种协议对应到一种类型。言下之意验证系统不支持程序员编写类似 qsort 这样的函数，因为 qsort 对作为形参的 compare 函数没有类型限定，只要能给出该类型两个元素的比较函数就可以。
  

• size_t 只能作为函数形参和返回值的类型，并且满足下面两点。
• 类型为 size_t 的形参，其对应实参的值正好是该函数某个形参的类型 t 的 sizeof(t)（也可以是 t 的元素的 sizeof(t[0]）。或者正好等于该函数某个指针型形参的类型 p 的 \length(p)。这两点约束必须以断言方式出现在函数的前条件中。
• 对于作为返回值类型的 size_t，该函数一定有形参，其类型和返回值的 size_t 类型相关，只要函数后条件正确写出了这个关系则可。例如：

//@ logic int n;
/*@ requires \is_pstring(str, n) && n <= INT_MAX;
    ensures \is_pstring(str, \result) && \result <= INT_MAX;
*/
size_t strlen(const char * const str);

　　C的语句标注（statement annotation）有两种：
　　1．程序点断言：允许出现在任何语句之前或者程序块的结尾。
　　2．循环标注：有 invariant 和 variant 两种，它们出现在 while、for 和do 语句之前。

　　图5.1 是C语句文法的扩展，其中非终结符 compound-statement、declaration 和statement 是C的非终结符，非终结符 assertion 和 loop-annot 等是为语句标注而扩展的。

5.1 程序点断言

5.1.1 assert断言

5.1.2 check断言

5.2 循环标注

5.2.1 循环不变式

5.2.2 循环变式

　　程序点断言 由关键字 assert 和 check 分成两种不同的用法 ，因为它们出现的位置相同（但不能同时出现在同一个位置），因此在本节中分成两小节来介绍。

　　assert 断言 的文法见图5.1。从文法可以看出，assert 断言可以出现在任何语句之前和程序块末尾语句之后。但是，程序点断言不能出现在循环语句之前的那个程序点，因为这里有循环不变式，可能还有循环变式。
　　assert Q 的含义是，Q 在当前状态下必须成立。当前状态是指程序正好执行到断言所在程序点的状态。并且Q 是作为当前程序点的断言，继续向下验证。
　　允许在任意程序点标注 assert 断言，会引起验证条件的增加。但是适当地在某些程序点标注断言，会给程序验证带来帮助：

1. 有助于程序员发现代码或断言中的错误。
2. 对于 if 和 switch 这类形成多个分支的语句，在这些语句之后的程序点标注 assert 断言，把这些分支的共同性质体现出来，在有些场合可以简化随后代码中的验证条件。
3. 往回跳转的 goto 语句被看成构成一个循环，程序员必须用 assert 断言的方式给出跳转所到达语句的前断言，作为该循环的循环不变式。

　　check 断言 可以出现在 assert 断言可以出现的地方。若当前程序点的断言是 P，check Q 的含义是，若 P ==> Q 得证，则把 P && Q 作为当前程序点断言，继续向下验证。check Q1, Q2; 的含义是，先证P ==> Q1，再证 P && Q1 ==> Q2。若两步都得证，则把 P && Q1 && Q2 作为当前程序点断言并继续向下验证；若仅前一步得证，则把 P && Q1 作为当前程序点断言并继续向下验证；若两步都未得证，则仍把 P 作为当前程序点断言并继续向下验证。
　　check 断言的一个重要用途是，若 P ==> Q 和 P && Q ==> R 都能证明，但因所用定理证明器的能力问题，P ==> R 就是证明不了，并且 R 不是一个需要归纳证明的性质。这时可用 check 断言方式进行帮助，可以免去显式引入引理 P ==> Q。
　　同样，check 断言暂时也只能用于不操作易变数据结构的代码。

　　循环标注的语法见图5.1。下面分别介绍循环不变式和循环变式。

　　一个简单的循环不变式标注如下：

1. 粗略地说，在整个循环开始执行之前，断言 I 成立。对于循环语句的三种形式，这个粗略的说法有细微的区别，分别仔细说明。
   （1）对于 while ( c ) s 循环，断言 I 在该语句之前程序点的状态中成立。
   （2）对于 for ( init; c; step ) s 循环，断言 I 在执行初始化表达式init 之后的状态中成立。
   （3）对于 do s while ( c ) 循环，断言 I 在第一次执行 s 之后的状态成立。
2. 断言 I 是归纳不变式。它的含义是，若 I 和 c 在某个状态中都为真，并且在这个状态下执行循环体能正常终止（或通过 continue 终止）在循环体的结束点，则 I 在结果状态中仍为真。 在不允许循环条件 c 有副作用的情况下，可以再精确描述为：
   　• 对于 while (c) s 循环，断言 I 必须由 s 保持。
   　• 对于 for (init; c; step) s 循环，断言 I 必须由 s 和随后的step 保持。
   　• 对于 do s while (c) 循环，断言 I 必须由 s 保持。
   

// 例5.1　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include<limits.h>

/*@ requires 0 < n <= INT_MAX && \length(t) == n;
	ensures \result == \max(0, n-1, (\lambda integer k. t[k])) &&\length(t) == n; 
				 // \max是高阶逻辑构造，见7.5节
*/
int max(int* const t, const int n) {
	int i = 0; int m, v;
	m = t[0];
	/*@ loop invariant
			0 < i <= n <= INT_MAX 
			&& m == \max(0, i-1, (\lambda integer k. t[k])) && \length(t) == n; 
	*/
	do {
		v = t[i++];
		m = v > m ? v : m;
	} while (i < n);

	return m;
}
						图5.2 查找一维数组中的最大值

// 例5.2-1　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <limits.h> 
#define CAPACITY 10000
int size = 0;
//@ global invariant capacity : 0 <= size <= CAPACITY; 		// 全局不变式，见第7章

int elements[CAPACITY+1];
/*@
	requires size >= 0 &&  size <= CAPACITY-1 &&  elements[0] == INT_MIN &&
			(\forall integer j:[1..size].elements[j] >= elements[j/2]) &&  x > INT_MIN;
	assigns elements, size;
	ensures size > 0 &&  size <= CAPACITY && 
			(\forall integer j:[1..size].elements[j] >= elements[j/2]);
*/
void insert(int x) {
	int i,t;
	size = size + 1; i = size; t = i / 2;

	/*@ loop invariant
		size > 0 && size <= CAPACITY && i == size && t == i/2 && elements[0] == INT_MIN &&
			x > INT_MIN && (\forall integer j:[1..size-1].elements[j] >= elements[j/2]) ||
		size > 0 && size <= CAPACITY && i <= size/2 && i > 0 && t == i/2 && elements[i] > x &&
			elements[0] == INT_MIN && x > INT_MIN &&
		(\forall integer j:[1..size].elements[j] >= elements[j/2]);
	*/
	while (elements[t] > x) {
		elements[i] = elements[t]; i = i / 2; t = i / 2;
	}
	elements[i] = x;
}
						  图5.3 二叉堆的插入函数

// 例5.2-2　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　

/*@	requires 
		size > 0 && size <= CAPACITY && (\forall integer j:[1..size].elements[j] >= elements[j/2]) &&
		\old(elements[1]) == elements[1];
	assigns elements, size;
	ensures size >=0 && size <= CAPACITY-1 && (\forall integer j:[1..size].elements[j] >= elements[j/2]) &&
		\result == \old(elements[1]);
*/
 int delete(){	/* 删除最小值 elements[1] */
	int i, child, lastElement, minElement;
	minElement = elements[1]; lastElement = elements[size]; size = size -1;
	if (size > 0) {
		i = 1; child = i * 2;
		if (child < size && elements[child +1] < elements[child]) {
			child = child + 1;
		}
		/*@	loop invariant
			size > 0 && size <= CAPACITY-1 && i > 0 && i <= size && child == i*2 && child < size && 
				elements[child] <= elements[child+1] && minElement == \old(elements[1]) &&
				(\forall integer j:[1..size].elements[j] >= elements[j/2]) && lastElement >= elements[i] ||
		 	size > 0 && size<= CAPACITY-1 && i > 0 && i <= size && child == i*2+1 && child <= size && 
				elements[child-1] > elements[child] && minElement == \old(elements[1]) &&
				(\forall integer j:[1..size].elements[j] >= elements[j/2]) && lastElement >= elements[i] ||  
			size > 0 && size <= CAPACITY-1 && i > 0 && i <= size && child == i*2 && child >= size &&
				minElement == \old(elements[1]) && lastElement >= elements[i] && 
				(\forall integer j:[1..size].elements[j] >= elements[j/2]);
		*/
		while (child <= size && lastElement > elements[child]) {
			elements[i] = elements[child]; i = child; child = i * 2;
			if (child < size && elements[child +1] < elements[child]) {
				child = child + 1;
			}
		}
		elements[i] = lastElement;
	}
	return minElement;
 }
 								图5.4 二叉堆的删除最小元函数

//例5.3
int x = 0; int y = 10;
/*@ loop invariant 0 <= x < 11; */
while ( y > 0 ) {
    x++;  y--;
}

　　下面介绍循环变式。循环变式用于验证循环不会陷入无限次迭代执行循环体，可粗略地称为循环终止。之所以不能正式称为循环终止，是因为终止还依赖于该循环内的调用语句都会返回，内循环都会终止。循环变式是可选的，若不使用则表示不要求对循环进行这种验证。若使用则其在循环标注中的形式是
//@ loop variant e;
其中e 是integer 或它的某个子类型的项。
　　它表示，对正常终止或通过 continue 终止的每次迭代，在迭代结束时 e 的值必须比同次迭代开始时 e 的值要小。并且 e 的值在每次迭代开始时必须非负。注意，e 的值在循环出口处可以是负数，这并不危及循环的终止。

　　例5.4 图5.5是循环变式的一个简单例子。
　　用其他的序而不是常见的整数上的序来描述终止性是可行的，在第6章进一步解释。
　　在循环嵌套的情况下，循环变式有一点使用的限制，就是内层循环的代码不得修改外层循环的循环变式中的变量。

//例5.4 
//@ requires -2 <= x <= 10;
void f(int x) {
    /*@
        loop invariant -2 <= x <= 10;
        loop variant x + 1;
    */ 
    while (x >= 0) {
        x -= 2;
    }
} //图5.5 一个简单的循环变式

　　程序的终止性 也是一个重要问题，它与循环语句以及递归函数调用都有关系。终止性是通过把每个循环和每个递归函数各联系到一个度量（measure）函数来保证的，其中有关循环的终止性在5.2.2节已经简单讨论过。若无特别说明，度量函数的表达式默认为整型，并且前后两次度量之间用整数上常规的序进行比较。也可以把度量函数定义到其他论域和/或使用不同的序关系。

6.1 整数度量

6.2 一般度量

6.3 递归函数调用

6.4 不终止的函数

　　函数的整数度量 采用语法为

// 例6.1
/*@	lemma property1: 
		\forall integer *b. \forall integer value. \forall integer k:[0..\length(b)-1]. 
			\length(b) > 0 && (\forall integer n:[0..\length(b)-2].b[n] < b[n+1]) && value > b[k]
	  ==> (\forall integer n:[0..k].value > b[n]);
	lemma property2: 
 		\forall integer *b. \forall integer value. \forall integer k:[0..\length(b)-1].
		\length(b) > 0 && (\forall integer n:[0..\length(b)-2].b[n] < b[n+1]) && value < b[k]
	  ==> (\forall integer n:[k..\length(b)-1].value < b[n]); 
*/

 #define MAX_LEN 10000
/*@	requires 0 < len <= MAX_LEN && \length(a) == len && (\forall integer n:[0.. len-2]. a[n] < a[n+1]);
	ensures 0 < len <= MAX_LEN && \length(a) == len && -1 <= \result && \result <= len-1 &&
			(\result >= 0 && a[\result] == val || \result == -1 && (\forall integer n:[0.. len-1]. a[n] != val)); 
*/
int bsearch(int* const a, int const len, int const val){
	int i, j, k; 
	i = 0;  j = len-1;

	/*@	loop invariant 
	 		0 < len <= MAX_LEN && \length(a) == len && 0 <= i <= len &&
 			-1 <= j <= len-1 && (\forall integer n:[0..len-2]. a[n] < a[n+1]) &&
			(j-i >= -1 && (\forall integer n:[j+1..len-1]. val < a[n]) && 
			(\forall integer n:[0..i-1]. val >a [n]) || j-i == -2 && k == i-1 && val == a[k]);
			loop variant j - i + 1; 
	*/
	 while(i <= j) {
		k = i + (j - i)/2;  if(val <= a[k]) j = k - 1;  if(val >= a[k]) i = k + 1;
	 }

	 if(j - i == -1) k = -1;
	 return k;
}
							图6.1 二分查找函数的代码及标注

　　除了整数度量外，更一般的度量可以使用关键字for 来建立在其他类型上。对于函数，语法形式为

// 例6.2　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <limits.h>
/*@	predicate lexico(int p1[2], int p2[2]) =
		p2[0] < p1[0] && 0 <= p2[0] && 0 <= p2[1] ||
		p2[0] == p1[0] && 0 <= p2[0] && p2[1] < p1[1] && 0 <= p2[1];
*/

//@	ensures INT_MAX >= \result >= 0;
int dummy ();	// 函数值大于或等于0

//@	requires INT_MAX >= x >= 0 && INT_MAX >= y >= 0;
void f(int x, int y) {
	//@ ghost int p[2]; 
	//@ ghost p[0] = x; p[1] = y;

	/*@	loop invariant INT_MAX >= x >= 0 && INT_MAX >= y >= 0 && p[0] == x && p[1] == y;	
	loop variant p for lexico;
	*/
	while (x > 0 && y > 0) {
		if (dummy () > 0) { 
			x--; y = dummy(); 
			//@ ghost p[0] = x; p[1] = y;
		} else { 
			y --; 
			//@ ghost p[1] = y;
		}
	}
}
						图6.2 使用字典序判断循环的终止

　　函数调用图上强连通的相互递归函数 称为一个函数簇。为便于以文件为单位的分模块验证，一个函数簇中的函数必须定义在同一个C文件中。在一个函数簇中，各个函数必须标注基于同一个关系R（从语法上看是同一个关系）的 decreases 子句。在该簇中的任意函数 f 的函数体中，任何对递归函数 g 的调用所在状态对 g 的度量（即 g 的度量项在该调用点的值），小于 f 函数开始状态中对f 的度量（即f的度量项在 f 开始点中的值）。这个原则也适用调用自身的直接递归场合。

　　例6.3 图6.3是经典的阶乘函数和斐波那契函数。
　　在斐波那契函数的两个递归调用点，验证函数入口时的度量与调用点的度量之间关系的验证条件如下（其中 \old(n) 表示 n 在函数入口点的值）：
n >= 0 && \old(n) == n && n != 0 && n != 1 ==> \old(n) > n-1 && n-1 >= 0，和
n >= 0 && \old(n) == n && n != 0 && n != 1 ==> \old(n) > n-2 && n-2 >= 0
　　如果该函数体缺少 n == 0 或者 n == 1 的分支，则这两个验证条件至少有一个得不到证明。

// 例6.3
//@logic int factorial(int n) = n > 0 ? n * factorial(n - 1) : 1;

/*@	requires 0 <= n <= 10; 
	decreases n;
	ensures \result == factorial(n);
*/
int fact(const int n) 
{
	if (n == 0) return 1;
	return n * fact(n-1);
}

/*@	logic int fibonacci(int n) = 
		n == 0 ? 0 : 
		(n == 1 ? 1 : fibonacci(n-1) + fibonacci(n-2));
*/

/*@	requires 20 >= n >= 0;
	decreases n;
	ensures \result == fibonacci(n);
*/
int fib(const int n) 
{
	if (n == 0 ) { return 0;
	} else if (n == 1) { return 1;
	} else { return fib(n-1) + fib(n-2); }
}

		图6.3 两个简单的直接递归函数

// 例6.4
#define N 10000
int odd(const int n);

/*@	logic int odd_l(int n);
	logic int even_l(int n) = n == 0 ? 1 : odd_l(n-1);
	logic int odd_l(int n)  = n == 0 ? 0 : even_l(n-1);
*/
/*@ requires n >= 0 && n <= N; 
	decreases n; 
	ensures \result == even_l(n);
*/
int even(const int n) {
	if (n == 0) return 1;
	return odd(n-1);
}

/*@ requires n >= 0 && n <= N; 
	decreases n; 
	ensures \result == odd_l(n);
*/
int odd(const int n) {
	if (n == 0) return 0;
	return even(n-1);
}							

						
			图6.4 相互递归的函数

　　在某些场合，函数就是要设计成不终止的。例如，反应式程序（reactive program）的 main 函数可能是 while(1)，它始终等待着下一个要处理的事件。更一般的情况是，函数可以在某些前条件得到满足时终止。在这种情况下，terminates 子句可以加到函数的协议中，其形式如下：
//@ terminates
以帮助验证函数在某些前条件得到满足时是否达到严格意义下的终止。
　　terminates p 子句的语义是，如果 p 为真，那么所属函数被保证终止（更准确地说系统必须证明它终止）。 如果不存在这样的子句（尤其是若所属函数根本没有函数协议），它默认为 terminates \true，也就是所属函数假设为一定终止，这是大多数函数被期望的行为。
　　注意，若 p 不为真，相当于什么也没有说，尤其是 terminates \false 并不暗示所在函数陷入无限循环。例如下面的函数就是不会终止的一种可能情况。

        /*@ ensures \false;
            terminates \false;
         */
        void f() { while(1); }

// 例6.5
//@ requires m ==\old(m) && m <= 0;
//@ terminates \old(m) <= 0;
void inc(int m) {
	//@ loop invariant m <= 0 && m >= \old(m);
	//@ loop variant -m;
	while(m != 0) {
		m = m + 1; 
	}
}
		图6.5 并非一定终止的函数

　　通过声明新的逻辑常量、逻辑变量、逻辑函数和谓词，可以扩展使用在标注中的逻辑表达式语言。这些声明的文法见图7.1。

7.1 逻辑定义和声明的作用域

7.2 逻辑常量和逻辑变量

7.3 谓词定义和函数定义

7.4 引理声明

7.5 高阶逻辑构造

7.6 宏定义

7.7 常用逻辑定义和引理组成的逻辑模块及其使用

　　逻辑定义和声明 若出现在C函数的外面，则它们的作用域是从定义或声明点到所在文件的结尾。对于需要被多个文件共享的部分，可以定义或声明在被它们包含的头文件中。与其它定义和声明不同的是，引理声明若出现在C函数的内部，则引理声明的作用域只从声明点到所在函数的结尾。对逻辑变量声明的一点额外限制见7.2节。
　　逻辑定义和声明出现的名字（有点像关键字的 logic, predicate, inductive, lemma, relies 和 on 除外），按作用域原则，不能与C代码部分的名字有冲突。

　　此外还需注意先定义后引用原则：

• 逻辑部分和C代码部分分别都遵循这个原则，C代码定义的名字可以在标注中引用，但必须先出现C的定义，然后才可以在逻辑定义和声明中引用C定义的名字。
• 对于逻辑定义和声明中出现的归纳谓词和归纳函数来说，由于可能出现间接归纳定义，因此允许先声明谓词和函数的原型，就像C的函数声明那样。

　　就像C的常量定义那样，逻辑常量定义也比较简单，被定义的常量在之后的标注中可以引用。对于逻辑常量声明 logic type-expr id = term 中 term 的语法约束是：只能出现直接量和先前已经声明的逻辑常量，以及可以操作于它们的算符。
　　SCSL中的逻辑变量可以用来表达程序对上下文的不变性质，这些性质用程序变量不足以表达。在Hoare逻辑中，程序断言表达程序变量在某个程序状态下的性质，难以描述程序变量在不同状态下的值之间的联系。若要用断言表达这种联系，使用逻辑变量是一种简单的解决办法。举个简单的例子，若不考虑机器能表示的最大整数有限制，若要表达无论当前 m 的值是多少，经过赋值 m = m + 2 后，m 的值总是增2。那么，若使用逻辑变量 oldm 表 示 m 的当前值，则可写出Hoare三元式 {oldm == m} m = m + 2 {oldm == m - 2}。oldm 的作用就是代表 m 原先的值。
　　在SCSL中，程序员声明的全局逻辑变量主要用来表达函数调用前后两个程序点的性质变化，因此一个逻辑变量同时出现在函数的前后条件中时才有实际意义。一个逻辑变量可以出现在多个函数的前后条件中，用于各自的目的。

　　逻辑变量的使用限制如下：

• 逻辑变量仅可以出现在断言中。
• 一个逻辑变量只有出现在函数的前条件中，它才可以出现在函数体中的循环不变式、程序点断言和函数的后条件中。这意味着不允许在函数体中声明局部的逻辑变量。
• 在函数前条件中，任意一个逻辑变量，只有其本身单独作为谓词应用的变元、逻辑函数应用的变元、量化断言区间的上下界或关系运算的一个运算对象（在此 0 <= x < 100 理解成一个或两个关系运算式都可以）后，才能出现在前条件的其他地方。可以理解为前者是逻辑变量的定义性出现（若有 t->level == m 和 t->l->level == m，其中 m 是逻辑变量，则择其一为定义性出现），其他地方的是引用性出现。一个谓词应用、逻辑函数应用、量化断言区间和关系运算最多只能有一个逻辑变量的定义性出现。
• 在描述逻辑变量定义性出现的关系运算中，关系运算的其他运算对象可以包括程序变量甚至量化断言。若是后者，则把整个量化断言理解成一个虚拟程序变量。在前条件中，这些程序变量尽量只用于逻辑变量的定义性出现的基本断言中，少出现在前条件的其他地方，以方便逻辑变量的匹配。
  　　逻辑变量的一种典型应用是表达函数调用的指针型实参在函数返回点具有的性质。由于C语言允许函数体对形参赋值，因此，在一般情况下，SCSL禁止不带 const 修饰符的形参出现在函数后条件中。这是因为不带 const 修饰符的形参可能被重新赋值，形参在函数返回点具有的性质不能作为实参在调用之后的性质。这时，逻辑变量可用来表达实参在函数调用之后具有的性质，或者表达其在调用前后的性质变化。
• 在函数前条件中，若指针型逻辑变量出现在等式断言中，则等式的另一端只能是程序指针变量，不能是程序指针加偏移的表达式。

// 例7.1　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
/*@	inductive sortedList(Node* p) =  p == \null || p->next == \null ||
			p->data <= p->next->data && sortedList(p->next);
			…
        logic Node* oldp;
*/
/*@	requires sortedList(p) && oldp == p;
	ensures sortedList (\result) && sortedList(oldp);
*/
Node* listCopy(Node* p){
	Node* q;
	…;
	return q;
}
				   图7.2 解释逻辑变量的使用

/*@ requires sortedList(p);
    ensures sortedList (\result) && sortedList(p);
*/
Node* listCopy(Node* const p){ ... }

// 例7.2　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdlib.h>
typedef struct node {
	int data;
	struct node* l;
	struct node* r;
}Node;
//@ shape l, r : tree;
/*@ inductive Gt(int succ, Node* p) =  
		p == \null || succ > p->data && Gt(succ, p->l) && Gt(succ, p->r);
	inductive Lt(int pred, Node* p) =  
		p == \null || pred < p->data && Lt(pred, p->l) && Lt(pred, p->r);
	inductive BST(Node* p) = 
		p == \null || 
		BST(p->l) && BST(p->r) && Gt(p->data, p->l) && Lt(p->data, p->r);
	lemma p1:
		\forall int pred1, int pred2, Node* p. pred1 < pred2 && Lt(pred2, p) ==> Lt(pred1, p);
	lemma p2:
		\forall int succ1, int succ2, Node* p. succ1 > succ2 && Gt(succ2, p) ==> Gt(succ1, p);
*/
/*@	logic int succ, pred; 
	logic Node* oldp; 
*/
/*@	requires 
		BST(p) && succ > data && Gt(succ, p) 
		&& pred < data && Lt(pred, p) && oldp == p;
		assigns *oldp;
	exits \exit_status == 1;
	ensures 
		BST(\result) && Gt(succ, \result) && Lt(pred, \result) 
		&& (oldp == \null || oldp == \result);
*/
Node* BSTInsert(Node* p, const int data) {
	if ( p == NULL){
		p = (Node *)malloc(sizeof(Node));
		if(p == NULL) exit(1);
		p->l = NULL; p->r = NULL; p->data = data;
	} else if (p->data > data){
		p->l = BSTInsert(p->l, data);
	} else if (p->data < data){
		p->r = BSTInsert(p->r, data);
	}
	return p;
}
	
							图7.3 二叉排序树的插入函数

// 例7.3
#include <stdlib.h>
typedef struct node {struct node *next; int data;} Node;
//@	shape next: list;
//@	logic int m; logic Node* oldhead;
/*@	requires
		\list(head) && \length(head, next) == m && oldhead == head && 0 <= m <= 1000 &&
		(\forall int i:[1..m-1].head->(next:i-1)->data <= head->(next:i)->data) &&
		\forall int i:[0..m-1].\old(head->(next:i)->data) == head->(next:i)->data;
	assigns oldhead;
	exits	\exit_status == 1;
	ensures	
		\list(\result) && \length(\result, next) == m+1 && oldhead == \result && 0 < m <= 1000 &&
			(\forall int i:[1..m].\result->(next:i-1)->data <= \result->(next:i)->data) &&
			(\exists int j:[0..m]. \result->(next:j)->data == data &&
			(\forall int i:[0..j-1]. \old(head->(next:i)->data) == \result->(next:i)->data) &&
			(\forall int i:[j..m-1]. \old(head->(next:i)->data) == \result->(next:i+1)->data)) ||
		\list(\result) && \length(\result, next) == m+1 && oldhead == \null && m == 0 &&
			(\forall int i:[1..m].\result->(next:i-1)->data <= \result->(next:i)->data) ||
		\list(\result) && \length(\result, next) == m+1 && oldhead ==\result->next && 0 < m <= 1000 &&
			(\forall int i:[1..m].\result->(next:i-1)->data<= \result->(next:i)->data)&&\result->data==data &&
			(\forall int i:[1..m-1]. \old(head->(next:i)->data) == \result->(next:i+1)->data);  
*/
Node* listInsert(Node* head, const int data) {
	Node *ptr, *ptr1, *p; int j;
	p = (Node*)malloc(sizeof(Node));
	if (p == NULL) { exit(1);}
	p->data = data; p->next = NULL;
	if (head == NULL) { head = p; }
	else if (p->data <= head->data){ p->next = head; head = p; }
	else{ ptr1 = head; ptr = head->next; j = 1;
		/*@ loop invariant 0 <= m <= 1000 && 1 <= j <= m && 
				oldhead == head && \list_seg(head, ptr1) && ptr1 == head->(next:j-1) && \list(p) &&
				\length(p, next) == 1 && ptr1->data <= p->data && p->data == data &&
				(  1<= j < m && ptr==ptr1->next && \list(ptr) && ptr != \null && \length(ptr, next) == m-j &&
				(\forall int i:[1..j-1].head->(next:i-1)->data <= head->(next:i)->data) &&
				ptr1->data<=ptr->data &&
				(\forall int i:[j+1..m-1].head->(next:i-1)->data <= head->(next:i)->data) &&
					(\forall int i:[0..j-1].\old(head->(next:i)->data) == head->(next:i)->data) && 
					(\forall int i:[j..m-1].\old(head->(next:i)->data) == head->(next:i)->data) ||
					j == m && ptr1->next == \null && ptr == \null &&
					(\forall int i:[1..m-1].head->(next:i-1)->data <= head->(next:i)->data) &&
					(\forall int i:[0..m-1].\old(head->(next:i)->data) == head->(next:i)->data)
				);
		*/
		while ((ptr != NULL) && (ptr->data < p->data)) {
			ptr1 = ptr;  ptr = ptr->next; 
			j = j + 1;
		}
		p->next = ptr1->next; ptr1->next = p;
	}
	return head;
}
								图7.4 有序单向链表的插入函数

• \old 构造在函数前条件中通过 \old(t) == t 的方式，用来记住函数的形参所对应的实参在函数入口点的值，也可用来记住会被函数修改的全局变量在函数入口点的值。在函数的前条件中，也可用逻辑变量等于全局变量或等于形参的断言来达到这个效果。
• 逻辑变量还具有 \old 构造取代不了的其他功能。这些逻辑变量出现在函数前条件的断言中，当它们用调用状态中适当的表达式代换时，能够使得调用状态满足函数前条件。见例7.2。
• \old 也可用于逻辑变量难以表达的地方，例如，例7.3用 \old 构造来记住链表各节点的数据在函数入口点的值。

　　逻辑函数和谓词 分别由表达式和断言显式地定义，出现在等号之后。表达式和断言中出现的变量都必须是相应定义的参数表中的变元。若出现间接递归的函数和间接归纳的谓词，则按照先定义后引用的原则，需适当地先给出其中某些函数和谓词的原型。图7.1中逻辑函数和谓词的文法给出了描述原型的可能。
　　在3.4节已经提到，逻辑函数和谓词的变元宜根据需求声明为C的合适类型，一般情况下不要使用逻辑类型 integer 和 real。

　　当数组和指针类型作为变元类型时，一些补充规定如下。

1. 数组类型可作为逻辑函数、谓词（包括归纳谓词，下同）和引理的变元类型，并且允许完整的数组描述和缺少数组大小的数组描述两种形式。

• 在逻辑定义 logic int f(array2 a)… 和 logic int f(int a[10][20])… 中，变元 a 的类型都有完整的描述，两个定义中 a 的类型都是 array2。这与C函数对形参的规定有区别，在C中，形参 a 的这两处声明都表示 a 是指针类型，是长度为20的一维整型数组的指针。这两个逻辑定义的变元是真正的数组，内建函数 \offset(a) 属性恒为0，\length(a) 等于数组的长度。应用这个逻辑定义的变元必须是同类型的数组。
• 在逻辑定义 predicate p(int a[][20], int len) = \length(a) == len && len > 0 && … 中，变元 a 的类型是缺少数组大小的二维数组类型，\offset(a) 属性仍然恒为0，这时必须还有另一个作为数组长度的变元，并且在定义体中有断言来描述数组长度受到的约束，例如 \length(a) == len && len > 0。允许用这种方式定义数组变元，是因为不能定义数组变元 int a[len][20]，其中 len 是变量。这种方式可用于允许数组 a 的长度任意的场合。应用这个逻辑定义的第一个实变元必须是数组，其元素的类型与该逻辑定义中第一个变元的元素类型相同。
  允许数组类型作为逻辑函数等的变元类型，是为了让逻辑函数等的定义或声明不出现指针，容易理解。
  
• 若需要写通用一些的逻辑定义，允许让逻辑定义中数组变元的元素类型为 integer，而该逻辑定义的应用中，相应的数组元素可以是 ingeger 类型的任意子类型。

2. 指针类型也可以作为逻辑函数、谓词和引理的变元类型，但受到较多的限制
   逻辑定义中实际上没有指针类型的变元，但C语言有指针类型。为方便程序员为C代码写标注，允许逻辑定义在下面两种情况下使用指针类型的变元。从逻辑定义的观点，这样的指针变元实际代表它指向的对象。
   （1）构造易变数据结构的自引用结构体或共用体类型的指针。从逻辑定义的角度，这种自引用类型的变量可以理解为，不再是通过指针域指向同类型的变量，而是把后者直接嵌入前者并取消前者的指针域。
   （2）在其他情况下，也允许使用 type* a 描述的指针变元，但这时的 a 实际上被看成数组，哪怕只有一个数组元素，还是因为逻辑定义中没有指针概念。这种方式与上述缺少长度信息的数组类型基本一样，唯一的区别是，\offset(a) 不一定是0，因此需用第三个变元表示。第3个变元的类型与该逻辑定义中第一个变元指向对象的类型相同。
   

• 若变元不是指针类型，但其分量是指针，这个分量同样被看成数组。
• 在逻辑函数和谓词的定义式和引理的声明中，不能出现指针运算符 "*" 和取地址运算符 "&"。
  作为指针类型的变元，它的声明中出现 "*" 则是另外一回事，因为这个 "*" 不是算符。这表明逻辑定义把变元声明 int a[10][20] 和 int a[][20] （包括上述 int* a[20]）中的变元 a 真正看成数组，而不像C那样把 a 看成数组元素的指针。需要强调一下，这是对逻辑定义的限制。指针运算符 "*" 和取地址运算符 "&" 是可以出现在函数协议、循环不变式和程序点断言等程序员给出的断言中的。
• 在内建函数中已多次用到 type* a 这样的指针变元。例如 predicate \is_pstring(char* str, int m)。

/*@ predicate is_positive(long x) = x > 0;
    logic int getSign(double x) = x > 0.0 ? 1 : (x < 0.0 ? -1: 0);
*/

/*@ inductive isGcd(long a, long b, long d) =
                b == 0 && a == d ||
                b != 0 && isGcd(b, a%b, d);
*/

/*@ logic int maxIndex(int t[], int n) =
              (n == 0) ? 0:
              (t[n-1] == 0) ? n : maxIndex(t, n -1);
*/

/*@ logic int smallest(Node* p) =
              (p->l == \null) ? p->data : smallest(p->l);
*/

　　引理 是程序员给出的断言，用以支持自动定理证明器来证明其他引理和/或验证条件的有效性。引理声明中引理名之后的括号中若有 both，则表示该引理既用于其他引理的证明，也用于验证条件的证明。若括号中有 relies on，则表示该引理本身的证明依赖于若干引理。both 和 relies on 可同时出现。若引理名之后的括号中没有 both，则表示该引理仅一种用途：若发现该引理被依赖，则它仅用于引理证明，否则仅用于验证条件的证明。下面是引理声明的一个简单例子。

/*@ lemma LtProperty:
	　　\forall int x. \forall int y. \forall Node* p. x < y && Lt(y, p) ==> Lt(x, p);
    lemma GtProperty: 
	　　\forall int x. \forall int y. \forall Node* p. x > y && Gt(y, p) ==> Gt(x, p);
*/

1. 引理中的整型约束变元，若其取值范围是闭区间的话，必须写成显式的区间约束。
   例如：　　　　\forall int i:[0..99].P(i) ，
   不必写成　　 　\forall int i. 0<=i<=99 ==> P(i)，
   
2. 引理中不同位置出现的常数，若它们在引理中的含义是相关联的，则必须用C的同一个宏定义或其他方式来表达它们的相关性。
   例如，
   
   #define N 100
   typedef int Dis[N];
   logic int count(Dis f, int m, int n) = n < m ? 0 : (count(f, m, n-1) + f[n-1]);
   lemma counting: \forall Dis f. \forall Dis oldf. \forall int u.
   　　　　(\forall int i:[0..u-1].oldf[i] == f[i]) && oldf[u] == 0 && f[u] == 1 &&
   　　　　(\forall int i:[u+1..N-1].oldf[i] == f[i]) && count(oldf,1,N) == i
   　　==> count(f,1,N) == i+1;
   
   而不要把引理写成：
   
   lemma counting: \forall Dis f. \forall Dis oldf. \forall int u.
   　　　　(\forall int i:[0..u-1].oldf[i] == f[i]) && oldf[u] == 0 && f[u] == 1 &&
   　　　　(\forall int i:[u+1..99].oldf[i] == f[i]) && count(oldf,1,100) == i
   　　==> count(f,1,100) == i+1;
   
   后者有可能导致引理自动证明的失败。
   
3. 所提供的引理能满足所在源文件或函数的验证即可，不必提供更一般的引理。例如，若一个引理仅用于某个C函数中某个或某些验证条件的证明，则把它声明在该函数的内部，放在声明语句之后的某个地方。

// 例7.9　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdlib.h>
typedef struct listnode { 
    int data; 
    struct listnode*r;  
    struct listnode* l;
} ListNode;
//@ shape l, r: dlist;
/*@ 
    inductive inc_sorted_seg(ListNode * p, ListNode * q) = 
        p == q && p != \null ||
        p != q && p->r->l == p && p->data <= p->r->data && inc_sorted_seg(p->r, q);
    redicate inc_sorted(ListNode * p) = 
        p == \null || p->l == \null && p->r == \null ||
        p->l == \null && \exists ListNode* q.inc_sorted_seg(p, q) && q->r == \null;
    predicate almost_inc_sorted(ListNode * p) = 
        \exists ListNode *q. inc_sorted_seg(p, q) && q->r == \null;
    inductive dec_sorted_seg(ListNode * p, ListNode * q) = 
        p == q && p != \null ||
        p != q && p->r->l == p && p->data >= p->r->data && dec_sorted_seg(p->r, q);
    predicate dec_sorted(ListNode * p) = 
        p == \null || p->l == \null && p->r == \null ||
        p->l == \null && \exists ListNode* q.dec_sorted_seg(p, q) && q->r == \null;
    predicate almost_dec_sorted(ListNode * p) = 
        \exists ListNode *q. dec_sorted_seg(p, q) && q->r == \null;  
        
    lemma inc_sorted_seg_push_back_lemma: \forall ListNode *p, ListNode *q.
        inc_sorted_seg(p, q) && q->r->l == q && q->data <= q->r->data ==> inc_sorted_seg(p, q->r);
    lemma dec_sorted_seg_push_back_lemma: \forall ListNode *p, ListNode *q.
        dec_sorted_seg(p, q) && q->r->l == q && q->data >= q->r->data ==> dec_sorted_seg(p, q->r);
    lemma inc_sorted_seg_pop_back_lemma: \forall ListNode *p, int n.
        n >= 0 && inc_sorted_seg(p, p->(r:n + 1)) ==> inc_sorted_seg(p, p->(r:n));
    lemma inc_sorted_seg_back_lemma: \forall ListNode *p, int n.
        inc_sorted_seg(p, p->(r:n + 1)) && n >= 0 ==> p->(r:n)->data <= p->(r:n + 1)->data;
    lemma dec_sorted_lemma: \forall ListNode *p, ListNode *q.
        dec_sorted_seg(p, q) && p->l == \null && almost_dec_sorted(q) ==> dec_sorted(p); 
*/

//@ logic integer n;
/*@ requires \length(list, r) == n && inc_sorted(list);
    assigns *list;
    ensures \length(\result, r) == n && dec_sorted(\result) &&
                (n > 0 && list == \result->(r:n-1) || n == 0 && list == \null);  
*/
ListNode * invert(ListNode * const list) /*@ shape ListNode forward: r;*/ 
{
    ListNode *last, *ptr, *tmp;
    //@ ghost int j;
    last = list;
    if (last != NULL) {
        //@ ghost j = 0;
        /*@ loop invariant 0 <= j < n && \dangling(ptr) && \dangling(tmp) &&
                list->l == \null && inc_sorted_seg(list, last) && last == list->(r:j) &&
                almost_inc_sorted(last) && \length(last, r) == n - j; 
        */
        while (last->r != NULL) { 
            last = last->r; 
            //@ ghost j = j + 1;
        }
        ptr = last;
        tmp = NULL;  
        //@ ghost j = 0;
        /*@ loop invariant
            n > 0 && j == 0 && list->l == \null && inc_sorted_seg(list, ptr) &&
                ptr == list->(r:n-1) && ptr == last && last->r == \null && tmp == \null 
            ||
            0 < j < n && list->l == \null && inc_sorted_seg(list, ptr) && ptr == list->(r:n-j-1) &&
                tmp == ptr->r && tmp->r == ptr && ptr->data <= tmp->data &&
                dec_sorted_seg(last, tmp) && tmp == last->(r:j-1) && last->l == \null 
            ||
            n > 0 && j == n && list->r == \null && dec_sorted_seg(last, tmp) &&
                tmp == last->(r:n-1) && tmp == list && last->l == \null && ptr == \null; 
        */
        while (ptr != NULL) {
            tmp = ptr->r; 
            ptr->r = ptr->l; 
            ptr->l = tmp; 
            tmp = ptr; 
            ptr = ptr->r; 
            //@ ghost j = j + 1;
        }
    }
    return last;
}
							图7.5 双向链表倒置（使用自定义谓词和引理）

// 例7.9　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdlib.h>

typedef struct listnode { 
    int data; 
    struct listnode*r;  
    struct listnode* l;
} ListNode;
//@ shape l, r: dlist;

//@import  \dist_module < ListNode( r:r, l:l ) > 
/*@ 
    using \inc_sorted_dlist_seg_push_back_lemma;
    using \dec_sorted_dlist_seg_push_back_lemma;
    using \inc_sorted_dlist_seg_pop_back_lemma;
    using \inc_sorted_dlist_seg_back_lemma;
    using \dec_sorted_dlist_lemma;
*/
//@ logic integer n;
/*@ requires \length(list, r) == n && \inc_sorted_dlist(list);
    assigns *list;
    ensures \length(\result, r) == n && \dec_sorted_dlist(\result) 
            && (n > 0 && list == \result->(r:n-1) || n == 0 && list == \null);
*/
ListNode * invert(ListNode * const list) /*@ shape ListNode forward: r;*/ 
{
    ListNode *last, *ptr, *tmp;  
    //@ ghost int j;

    last = list;
    if (last != NULL) {
        //@ ghost j = 0;
        /*@ loop invariant 0 <= j < n && \dangling(ptr) && \dangling(tmp) 
            && list->l == \null && \inc_sorted_dlist_seg(list, last) && last == list->(r:j) 
            && \almost_inc_sorted_dlist(last) && \length(last, r) == n - j;  
        */
        while (last->r != NULL) {
            last = last->r;  
            //@ ghost j = j + 1;
        }
        ptr = last;  tmp = NULL;  
        //@ ghost j = 0;
        /*@ loop invariant
            n > 0 && j == 0 && list->l == \null && \inc_sorted_dlist_seg(list, ptr) 
                && ptr == list->(r:n-1) && ptr == last && last->r == \null && tmp == \null 
            || 0 < j < n && list->l == \null && \inc_sorted_dlist_seg(list, ptr) 
                && ptr == list->(r:n-j-1) && tmp == ptr->r && tmp->r == ptr 
                && ptr->data <= tmp->data && \dec_sorted_dlist_seg(last, tmp) 
                && tmp == last->(r:j-1) && last->l == \null 
            || n > 0 && j == n && list->r == \null && \dec_sorted_dlist_seg(last, tmp) 
                && tmp == last->(r:n-1) && tmp == list && last->l == \null && ptr == \null; 
        */
        while (ptr != NULL) {
            tmp = ptr->r; 
            ptr->r = ptr->l; 
            ptr->l = tmp; 
            tmp = ptr; 
            ptr = ptr->r; 
            //@ ghost j = j + 1;
        }
    }
    return last;
}
							图7.5 双向链表倒置（使用内置谓词与引理）

　　项 \lambda τ₁ x₁, ..., τ_n x_n. t 称为抽象，它代表n 元的逻辑函数，其参数是 x₁, ..., x_n，它们的类型分别是τ₁, ..., τ_n，函数体是t。\lambda 的优先级同 \forall 和 \exists 的一样。在SCSL中，\lambda 抽象作为函数类型的表达式，它目前仅用作下面所列扩展范域词的第3个变元。
　　forall、exists 和 lambda 统称为范域词（quantifier），其中全称范域词forall 和存在范域词exists 习惯称为全称量词（universal quantifier）和存在量词（exist quantifier），lambda 可称为抽象范域词。在形式为 \quant(t₁, t₂, t₃) 的项中，quant 是扩展范域词，目前只有 max、min、sum、product 和 numof 五个扩展范域词。变元t₁ 和t₂ 必须是integer 类型或它的子类型，t₃ 必须是变元为integer 类型或它的子类型的一元函数。在numof 中，一元函数t₃ 的结果是布尔值，其余各函数的一元函数t₃ 的结果是integer 或real 类型或它们的子类型。函数t₃ 的类型不是显式声明的，它是由对t₃ 表达式本身进行推导得到的。它们的含义如下：

// 例7.10　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#define N 1000
/*@	requires N >= n >= 0 && \length(t) == n;
	ensures \result == \sum(0, n-1, \lambda int k. t[k]) && \length(t) == n;
*/
double array_sum(double* const t, const int n) {
	int i;  double s = 0.0;
	/*@	loop invariant 0 <= i <= n <= N && s == \sum(0, i-1, \lambda int k. t[k])  && \length(t) == n;
		loop variant n - i;
	*/
	for(i = 0; i < n; i++) s = s + t[i];
	return s;
}
								图7.6 一维数组求和

// 例7.11　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
const int m = 100; const int k = 200; const int n = 300;
typedef int AB[100][200];
typedef int BC[200][300];
typedef int AC[100][300];
AC Z = {0};
// 谓词定义
/*@ predicate element(AB X, BC Y, AC Z, int i, int j, int l) = 
		(Z[i][j]==\sum(0, l-1, \lambda int l1.X[i][l1]*Y[l1][j]))
		&& -3000*3000*l <= Z[i][j] <= 3000*3000*l;
		// 元素Z[i][j]的值的计算已经累加了X[i][l-1] * Y[l-1][j]
predicate column(AB X, BC Y, AC Z, int i, int j) = 
		\forall int j1: [0..j-1]. element(X, Y, Z, i, j1, \dimension(X, 2));
		// 在第i行中，元素Z[i][0], ..., Z[i][j-1]的值都已算好
predicate row(AB X, BC Y, AC Z, int i) =
		\forall int i1: [0..i-1]. column(X, Y, Z, i1, \dimension(Y, 2));
		// 数组Z从0到i-1各行的元素的值都已算好
predicate matrixMultiply(AB X, BC Y, AC Z) = row(X, Y, Z, \dimension(X, 1));
		// 数组Z的所有行都已经算好 */

// 函数协议
/*@ 	requires m == 100 && k == 200 && n == 300 && \length(X) == m && \length(Y) == k &&
		(\forall int i:[0..99]. \forall int j:[0..199]. -3000 <= X[i][j] <= 3000) &&
		(\forall int i:[0..199]. \forall int j:[0..299]. -3000 <= Y[i][j] <= 3000);
	assigns Z;
	ensures matrixMultiply(X, Y, Z) && \length(X) == m && \length(Y) == k; 
*/
void MatrixMultiply1(int (*const X)[200], int(*const Y)[300]) 
{
	int i, j, l;
	/*@ loop invariant 0 <= i && i <= m && row(X, Y, Z, i) && m == 100 && k == 200 && n == 300 &&
			\length(X) == m && \length(Y) == k &&
			(\forall int i:[0..99]. \forall int j:[0..199]. -3000 <= X[i][j] <= 3000) &&
			(\forall int i:[0..199]. \forall int j:[0..299]. -3000 <= Y[i][j] <= 3000);	
		loop variant m - i; 
	*/
	for (i = 0; i < m; i = i + 1) {
		/*@ loop invariant 0 <= i && i < m && row(X, Y, Z, i) && 0 <= j && j<=n &&
				column(X, Y, Z, i, j) &&m == 100 && k == 200 && n == 300 && \length(X) == m &&
				\length(Y) == k &&
				(\forall int i:[0..99]. \forall int j:[0..199]. -3000 <= X[i][j] <= 3000) &&
				(\forall int i:[0..199]. \forall int j:[0..299]. -3000 <= Y[i][j] <= 3000);
			loop variant n - j; 
		*/
		for (j = 0; j < n; j = j + 1) {
			Z[i][j] = 0;
				/*@ loop invariant 0 <= i && i < m && row(X, Y, Z, i) && 0 <= j && j < n &&
					column(X, Y, Z, i, j) && 0 <= l && l <= k && element(X, Y, Z, i, j, l) &&
					m == 100 && k == 200 && n == 300 && \length(X) == m && \length(Y) == k &&
					(\forall int i:[0..99]. \forall int j:[0..199]. -3000 <= X[i][j] <= 3000) &&
					(\forall int i:[0..199]. \forall int j:[0..299]. -3000 <= Y[i][j] <= 3000); 
			*/
			for (l = 0; l < k; l = l + 1) {
				Z[i][j] = Z[i][j] + X[i][l] * Y[l][j];
			}
		}
	}
	return;
}		
									图7.7 矩阵相乘函数及协议

　　宏定义和宏应用 类似C语言中的宏定义和宏调用，也分成无参数和有参数两种情况，在语法上和C的略有区别（见图7.1）。

1. 无参数的宏定义

2. 带参数的宏定义

　　对于在程序验证中 常用的一些逻辑定义和引理，按照C语言的类型，或类型的运算，或基于C的类型构造的数据结构，分门别类地组织成各种逻辑模块，以方便写标注时引用它们。 一个逻辑模块中除了有引理外，还可能有这些引理中用到的逻辑定义，一个逻辑模块中也可能只有逻辑定义而无引理。
　　导入声明的关键字 import 之后跟随内建模块名，即图7.1文法中第1个 id，可能有的第2个 id 是该程序中自引用结构体的类型名， 可能有的随后的 id : id 是指模块中自引用结构体和程序中自引用的结构体类型之间域名的对应。这样将id:id中的对应顺序规定下来，即第一个id必须是模块中的域名，第二个id必须是程序中自引用结构体的域名。 导入声明表示把这些模块的逻辑定义和引理依次展开在这个导入声明处，取代导入声明。并依据声明中的域名对应表，进行模块中自引用的结构体类型中的域名到程序中自引用结构体域名的代换。 展开后的逻辑定义和引理的作用域遵循7.1节的规定。
　　使用声明的关键字 using 之后跟随内建引理名以及可能有的该程序中自引用结构体的类型名。与导入声明不一样的是，一个 using 之后可以跟随若干个内建引理。 另一个不同是这里不需要给出域名之间的对应，因为在导入声明时已经给出。使用声明表示代码中相关位置验证条件的证明很可能要用到这些内建引理。 若使用声明出现在函数内部，则表示从这个位置到函数末尾的验证条件，系统都会加上这个声明中的内建引理来证明这些验证条件。 若使用声明出现在函数外部，则表示从这个位置到文件末尾的验证条件，系统都会加上这个声明中的内建引理来证明这些验证条件。
　　在图3.1项文法和图3.2断言文法中出现的 \result、\old、\dimension、\pointer、\list、\c_list、\is_string 和 \prefix 等逻辑定义，都是系统内建的定义，它们无须导入就能使用。
　　可供程序员导入并使用的逻辑模块请见附录一。这些模块中的引理是已经证明过的，导入时无需证明。在使用导入声明时，请确认拟导入模块中的逻辑定义和引理是否为自己所需。 若略有差异，例如变元的类型或表达式中的算符不同，则不要导入该模块。

　　程序员若用标注指明某类型的所有变量在其生命周期中始终存在的性质，或者并非始终存在但在关键程序点存在的性质，这会给程序验证带来方便。这样的标注称为类型不变式。程序员也可以标注一个类型的某个变量所具备的特殊性质，这样的标注称为变量不变式。类型不变式和变量不变式统称为数据不变式。
　　对于用以构造易变数据结构节点的数据类型，程序员需要标注这些数据类型用以构造的易变数据结构的形状等信息。这种标注称为形状标注。

8.1 类型不变式

8.2 变量不变式

8.3 易变数据结构的形状标注

8.3.1 描述形状性质的指针断言的种类及基本限制

8.3.2 各种易变数据结构的形状标注

8.3.3 对函数协议和循环不变式等的指针断言和节点数据断言的限制

8.3.4 形状标注和形状特征断言小结

　　类型不变式可以标注到全局定义的类型 τ 上，τ 类型的任何外部变量和静态外部变量（也包括外部变量和静态外部变量的域或数组元素等属于 τ 类型的情况）都遵守类型不变式的规定。类型不变式有强弱之分。 全局定义的静态类型（指该类型的变量将分配在静态数据区。对于动态分配在栈区或堆区的数据，考虑其类型不变式是没有意义的），该类型的任何变量遵守类型不变式的规定。类型不变式有强弱之分。

1. 强类型不变式必须在程序执行的任何时候（更精确地说，是在C标准定义的任何顺序点（sequence point））都有效。若该函数的返回值属于 τ 类型，则返回值在函数出口必须满足 τ 的强类型不变式。
2. 弱类型不变式必须在函数的边界（函数的入口和出口）有效，但不要求在这两点之间保持有效。若该函数的返回值属于 τ 类型，则返回值在函数出口必须满足 τ 的弱类型不变式。

1. 类型为 temperature 的变量的强类型不变式 如下：

typedef double temperature;
//@ strong type invariant temp_in_celsius (temperature t) = t >= 273.15;

2. 类型为 struct S 的变量的弱类型不变式 如下：

struct S {
    int f;
}
//@ type invariant S_f_is_positive(struct S s) = s.f >= 0;

3. 若类型为 struct S 的变量的类型不变式修改如下：

struct S {
    temperature f;
}
//@ strong type invariant S_f_is_positive(struct S s) = s.f >= 0.0;

4. 对于指针类型 τ1，其类型不变式主要描述 τ1 指针所指向数据区的长度和指针的偏移，而 τ1 指针所指向对象类型 τ2 的不变式，应该描述在 τ2 类型处，因为这是另一个类型。

#define N 100
typedef enum {BLUE, WHITE, RED} color;
//@ type invariant isColor(color c) = c == BLUE || c == WHITE || c == RED;

typedef struct flag{int n; color* colors;}flag;
/*@ strong type invariant is_colored(flag f) =
        0 < f.n <= N && \length(f.colors) == f.n && \offset(f.colors) == 0 &&
        \forall integer k. 0 <= k <= f.n <= N ==> isColor(f.colors[k]); 
*/

1. 构造类型A 的分量（包括构造类型和指针类型的分量）若有不变式，则这些不变式都是A 的类型不变式的一部分。若类型A 还是某个类型的某个分量的类型，则A 的类型不变式就是该类型的不变式的一部分。
2. 若A 类型的分量B 是指针类型，指向的对象类型为C，则需要把C 类型的不变式作用到B 指向的对象之后的公式作为A 类型的不变式的一部分。除非C 类型没有不变式。见例8.1的第4例。
3. 若A类型的分量B 属于构造类型C，则需要把C 类型的不变式作用到B之后的公式作为A 类型的不变式的一部分。除非C 类型没有不变式。见例8.1的第3例。

　　变量不变式 可以标注到外部变量、静态外部变量和静态局部变量，表达在其生命周期中始终存在的性质。变量不变式也有强弱之分。

1. 强变量不变式表示被标注的变量在程序执行的任何时候都有效。因此强变量不变式表示这些变量在执行过程中的任何一步都必须保持的性质。
2. 弱变量不变式表示被标注的变量在函数的边界有效，但不要求其在这两点之间保持有效。因此弱变量不变式表示这些变量在任何函数的入口和出口的性质。
无论是带上述哪种变量不变式，变量都必须在声明时置初值。一个例外是在多源文件共享时，变量不变式定义在共享头文件中该变量的extern声明处，变量的初值则在变量定义的源文件中给出，如例8.2中的例2。


3. 和类型一样，一个变量不可以有多个变量不变式，也不允许同时受类型不变式和变量不变式的约束。
4. 变量不变式是否需要出现在函数协议和语句标注中，与类型不变式的情况一致。

1. 全局弱变量不变式 a_is_positive，它表示全局变量 a 必须维持为正的，但是 a 在函数调用和返回的区间可以违反这个性质。

int a = 1;
//@ global invariant a_is_positive: a > 0;

2. 全局强变量不变式 m_eq_100，它表示全局变量始终等于100，任何情况下不会改变。稍许复杂一些，它涉及3个C源文件 const.h、const1.c 和 const2.c，它们有关的内容分别如下：

const.h:
    extern int m;
	//@ strong global invariant m_eq_100: m == 100; // 标注出现在头文件中了，
	// 包含该文件的其他文件就不用再为m 定义全局不变式，定义了反而会报错。
    …  …
	
const1.c:
    #include "const.h"
    int m == 100;         // 在本文件中定义m，但无需标注
    …  …
	
const2.c:
    #include "const.h"    // 该文件中引用m，也无需标注

// 例8.3（1）
	void out_char(char c) {
		static int col = 0;
		//@ global invariant I : 0<=col<=79;
		col ++; 
		// 当col == 80 时不满足变量不变式
		if (col >= 80) col = 0;
	}
		  图8.2 一个静态局部变量的不变性

// 例8.3（2）
	void out_char(char c) {
		static int col = 0;
		//@ global invariant I : 0<= col <=79;
		// 当col == 79 时，col被重置为0，变量不变式始终满足
		if (0 <= col && col < 79) col++; 
		else col = 0;
	}
		图8.2 一个静态局部变量的不变性

　　形状 是对易变数据结构的一种分类，这种分类反映易变数据结构的形状特征。例如双向链表和二叉树分别都是节点之间链接关系相同的一类易变数据结构的总称。形状系统是一组规则，它指派形状属性给各种各样的易变数据结构。
　　为易变数据结构设计形状系统的目的是，限制程序可以构造和使用的易变数据结构的种类，达到既能满足绝大多数实际软件编程的需要，又能禁止程序员随意构造难以分析和验证其性质的易变数据结构。通过这样的形状系统，控制住易变数据结构的复杂性，提高指针操作程序的合法性门槛，便于排除没有构造出（或没有操作在）程序员所声明形状上的程序，降低程序分析和程序验证的难度。
　　形状系统 要求程序员声明结构体类型或共用体类型用于构造的易变数据结构的形状。易变数据结构的形状声明可类比变量的类型声明，不同的是，形状声明比变量的类型声明复杂，并且形状声明以标注形式出现在程序注释中。
　　在程序验证中，形状声明有助于程序员在函数前后断言、循环不变式和程序点断言中描述单态和多态命名基本形状中各节点的指针特性，还有助于程序验证系统发现程序中的指针错误。
　　形状系统在《安全C语言使用手册》的第3章已经介绍，本节介绍怎样在易变数据结构的节点的类型声明和相关的指针变量声明之后进行形状标注。形状标注的文法见图8.4。

　　对于程序员给出的、描述形状性质的指针断言，包括对出现在节点数据性质断言中的指针类型的前缀（以下都简称指针断言），存在一些限制。
　　首先对作为指针的堆指针访问路径作一些限制。
　　（1）在用断言整体描述（见8.3.3节）双向链表和带环链表的形状时，访问路径不能出现环。例如，双向链表上，p->r->l->r 和 p->r->r->l->l->r 都有环，因为它们都是语义上与 p->r 一样的访问路径。
　　有一种情况不受这个限制。在定义谓词、归纳谓词和逻辑函数以及声明引理时，允许出现 p->r->l 这样的访问路径。以例7.6双向链表倒置的图7.5为例，其中的归纳谓词定义和引理声明中都出现断言 p->r->l == p，其中构成小环的访问路径 p->r->l 是无法用其它无环访问路径替代的。好在这是在定义或声明中用于表达构成小环这种性质，不是在程序点的断言中。
　　（2）若访问路径带折迭域，例如，p->(next:e)->data，其中e 是非负线性整型表达式并且其中不含对堆指针指向对象的访问，则称该访问路径为含折迭域的访问路径。一条堆指针类型的访问路径上最多出现一次折迭域，并且该指针域是这条访问路径的最后一个指针域。
　　对于作为节点数据域访问路径前缀的堆指针访问路径同样受上述两点限制。
　　对于程序员在标注中给出的堆指针访问路径，包括其后还有访问其指向节点数据域的情况，再增加下面两点约定。
　　（1）在程序员给出的标注中，若从 p 指向节点到 q 指向节点有一条路径，则称 q 依赖于 p。
　　（2）在谓词定义、性质引理和逻辑函数的定义中，以及在函数前后条件、循环不变式和程序点断言中，若在一组合取的断言中出现 p->next 或 p->data 这样的访问路径，则默认在这组合取的断言中有合取子句 p != \null，不管该断言是否显式给出。经常需要提醒，这里的p 并非一定是指针型的声明变量，它可以是复杂一些的指针型访问路径。

　　指针断言最终体现出的是表达指针相等与否的断言（包括是否等于\null，是否为悬空指针，是否为单节点指针），从语法特点上说，可以概括为以下几种形式。
　　（1）简单指针断言
　　直接是指针相等与否断言，等号或不等号的两边是指针型简单访问路径。简单访问路径是指访问路径中没有程序函数和幽灵函数的应用，没有逻辑函数应用，也不出现折迭域。
　　（2）含折迭域的指针断言
　　在简单指针断言中出现含折迭域的访问路径。对于简单指针断言和含折迭域的简单指针断言，建议把相对简单的访问路径（尤其是指针型声明变量时）放在等号或不等号的左边。
　　（3）含逻辑函数应用的指针断言
　　在指针相等与否的断言中，若等号或不等号两边的访问路径表达式含结果是指针类型的逻辑函数应用，则称它为含逻辑函数应用的指针断言。例如 p == rightMost(succ->l)，其中 rightMost 的定义是：

几点限制 如下。

• 内建形状谓词（例如 \dangling(p) 和 \singleton(p)）不能出现在程序员定义的谓词和归纳谓词中。
• 对于程序员定义的谓词，若有 p 和 q 两个指针变元，并且 q 依赖于 p，则在谓词的变元表中，p 必须先于 q。
• 在谓词定义中，不能出现没有依赖关系的指针进行比较。没有依赖关系意味着它们指向不同的易变数据结构。

　　基本形状 基本形状分成单态和多态两类。图8.4文法中的非终结符 shape_decl 那一行列出了系统所允许的各种基本形状。单态基本类型分成单态命名基本形状和单态无名基本形状两种。

1. 单态命名基本形状

• 在循环或递归代码中按 forward 指针域的前进方向遍历节点。
• 在用量化断言或归纳谓词来逐点描述相邻节点的数据关系（例如递增链表）时，forward 指针域出现在这些节点的访问路径上。
一般来说，这两种情况下用的 forward 指针域确实是同一个。下面再说如何给出这样的标注。


• 对于操作双向链表或/和循环双向链表的每个函数，需要通过形状标注指明本函数是按哪个指针域来遍历易变数据结构的节点的。该指针域也是标注中访问节点数据所使用的访问路径上允许出现的指针域。
　　对于例7.9双向链表倒置的函数 invert，从该函数的代码可知，指针域r 的前进方向就是 forward 方向。所以 forward 标注应该如下（见图8.4的文法）：

ListNode* invert(ListNode* const list)/*@ shape ListNode forward : r; */{ … }

在该例的有序链表和表段的定义中，相邻节点的数据大小比较，也是以 r 为前进方向的。
　　若仅是函数原型，这样的形状标注仍然出现在参数表之后。


• 使用这种节点数据类型的不同函数，可以确定各自的 forward 指针域。
  若需要在一个函数中操作使用这种节点类型构造两个链表（例如两个双向链表），并且它们的 forward 指针域不同，则需要用 typedef 方式为类型 ListNode 定义另一个名字，例如 Node1，让其中一个链表的节点使用 Node1 类型。这是标注 /*@ shape ListNode forward : r; */ 中需要出现节点类型名的原因。
• 在r 为forward 域的情况下，在程序员的标注中，p->r->data == 10 和 p->data < p->r->data 都是允许的，p->r->l->r->data == 10 和 p->data < p->r->l->r->data 都是不允许的。虽然后两者与前两者在语义上是一样的。

2. 单态无名基本形状

• 指向子节点的边为正向边。
• 指向祖先节点的边为逆向边。
• 互不以对方为祖先的两个节点之间的边为交叉边。

3. 多态基本形状

4. 嵌套形状

5. 含内部附加指针的形状

// 例8.5　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
typedef struct node{struct node *child, *sib, *parent, *sib_prev;} Node;
/*@	shape child, sib : tree, primary;
	shape parent, sib_prev: tree, invariant;
	inductive mcf_tree(Node* s) = 
	   (s->sib!= \null ==> s->sib->sib_prev== s && s->sib->parent == s->parent && mcf_tree(s->sib)) &&
	   (s->child != \null ==> s->child->parent==s && s->child->sib_prev == \null && mcf_tree(s->child));
	type invariant mcfTree(Node* s) = s == \null || s->parent == \null && mcf_tree(s);
*/
					图8.5 含两个逆向指针的左孩子右兄弟树的节点的类型定义和标注

// 例8.6　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#define M 5				// B-树的阶
typedef struct BTNode {
	int keynum;			// 节点中关键字个数，即节点的大小
	struct BTNode* parent;	// 指向双亲节点
	int key[M+1];			// 关键字向量，key[0]单元未用
	struct BTNode* ptr[M+1];	// 子树指针向量
	//@ ghost int hight;		// 树的高度
}BTNode, *BTree;			// B-树节点和B-树的类型
/*@	shape ptr : no_name, primary;
	shape parent : no_name, invariant;

	inductive Lt(integer key, Btree t) = t == \null || k < t->key[1] && Lt(k, t->ptr[0]);
	inductive Gt(integer key, Btree t) = t == \null || k > t->key[t->keynum] && Gt(k, t->ptr[t->keynum]);
	inductive B_Tree(Btree t) = t == \null ||
		(t->parent == \null ==> 2 <= t->keynum <= M-1) 
	 &&	(t->parent != \null ==> (M+1)/2 <= t->keynum <= M-1) 
	 &&	(t->hight == 1 ==> (\forall integer i:[0..keynum]. t->ptr[i] == \null)) 
	 &&	(t->hight > 1 ==> (\forall integer i:[0..keynum]. t->ptr[i] != \null 
					t->ptr[i]->hight == t->hight-1 &&  t->ptr[i]->parent == t))  
	 &&	(\forall integer i:[keynum+1..M]. t->ptr[i] == \null) 
	 &&	(\forall integer i:[1..keynum-1].t->key[i] < t->key[i+1]) 
	 &&	(\forall integer i:[1..keynum].Gt(t->key[i], t->ptr[i-1]) && Lt(t->key[i], t->ptr[i]));

	type invariant B_Trees(BTree t) = t == \null || t->parent == \null && B_tree(BTree t);
*/
							图8.6 B-树的类型和标注

6. 含外来附加指针的形状

typedef struct node {int data; struct node *next;} Node;
//@	shape next: list;

typedef struct queue{Node *front, *rear;} Queue;
/*@	type invariant queuePred (Node *q) = 
	q->rear == \null && q->front == \null || 
	\exists integer n.(\length(q.front, next) == n && q.rear == q.front->(next:n-1));
*/
					图8.9 队列的类型定义和标注

7. 相同形状实例的序列

8. 单个节点的使用

　　在函数前后条件、循环不变式和程序点断言中，需要用断言把形状特征描述清楚，就是把相应形状图上的堆指针的有效性和其中有效指针之间的相等性描述清楚。对描述所使用的断言，在8.3.1节的基础上，还有进一步的限制。

1. 形状的描述方式

• 若合取的所有断言不引用该链表任何节点的其他域（非构造链表的指针域），则该链表可以分段描述也可以整体描述。否则必须分段描述，原因见下面描述形状所使用的各类断言的第（6）点。
• 在整体描述一个形状图时，对于描述外来指针之间距离的分段和以 head 为基准这两种方式，只能选用一种，不要混用。另外，在分段描述一个形状图时，不允许使用以 head 为基准的方式。

2. 描述形状所使用的各类断言

• 含折迭域的指针断言 只能是等式断言，并且含折迭域的访问路径只能出现在等号的一侧，例如 p == head->(next:m-1) 和 q->next == head->(next:m-1) 分别表示从 head 指向节点到 p 指向节点和从 q->next 指向的节点都经过 m-1 个 next 指针域。不要认为后者可以简化成 q == head->(next:m-2)，因为 q->next 可以是经过一个不在 head->(next:m-1) 这条路径上的一个节点再指向 head->(next:m-1) 的。

• 若是指向并不构成形状的单个节点的指针，则用断言 \singleton(p) 表示。也许还有进一步描述p 指向节点的域指针的描述。\singleton(p) 的变元 p 不允许有折迭域。
• 若指针 q 是悬空指针，则用断言 \dangling(q) 表示，同样，也不能有 q 等于某个指针的等式断言。

• 不得使用含逻辑函数应用的指针断言。
• 不得使用量化的指针关系断言。

• 对于整体描述的形状，用一个长度断言给出链表的表长，例如从
  
  \list(head) && p == head->(next:m-1) && q == p->(next:1) &&
  　　　　　　　　\length(head, next) == m+n
  
  可知表长为 m+n。
• 对于分段描述的形状，用各分段长度之和作为整个形状的长度。例如，从
  
  \list_seg(head, p) && q == p->next && \list(q) &&
  p == head->(next:m-1) && \length(q, next) == n
  
  可知表长为 m+n。也就是这个分段描述默认了表长为 m+n。
• 在分段描述方式中，各分段的描述和各分段的长度描述必须一致，即两者对形状的分段是一致的。例如 \list_seg(p, q) 的描述和长度描述 q == p->(next:n) 是一致的。

• 若形参p 是const 指针，则p 可以出现在后断言中，它描述的就是实参指针的性质。例如，函数后条件中应该有断言 \dangling(p)。见《安全C语言使用手册》的例3.15。
• 若形参 p 是指针，但没有修饰符限定 p 在函数中不能被赋值，从前条件的限制知道，前条件中有断言 oldp == p，则函数后条件中可用 oldp 来描述实参指针。例如，函数后条件中有断言 \dangling(oldp)。

3. 描述形状中各节点数据所使用的断言

// 例8.7　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdlib.h>
typedef struct node{ struct node* next; int data;} Node;
//@	shape next: list;
//@	logic Node* oldhead;
/*@	inductive sorted_list(Node * p) =
		p == \null || p->next == \null || p->data <= p->next->data && sorted_list(p->next);
	inductive sorted_seg(Node * p, Node * q) =
		p == q && p != \null || p != q && p->data <= p->next->data && sorted_seg(p->next, q);
*/
/*@	lemma property1: \forall Node* p, Node* q.
		sorted_seg(p, q) && q->data <= q->next->data && q->next != \null ==> sorted_seg(p, q->next);
	lemma property2: \forall Node* p, Node* q. 
		sorted_seg(p, q) && sorted_list(q) ==> sorted_list(p); 
*/
/*@	requires 
		sorted_list(head) && \list(head) && \length(head, next) == m && oldhead == head;
	assigns *oldhead;
	exits \exit_status == 1;
	ensures 
		sorted_list(\result) && \length(\result, next) == m + 1 
		&& (m > 0 && oldhead == \result || m == 0 && oldhead == \null 
			|| m > 0 && oldhead == \result->(next:1)
			)
		;
*/
Node * listInsert(Node * head, const int data, const int m)
{
	Node *ptr, *ptr1, *p;
	//@ ghost int j;

	p = (Node*)malloc(sizeof(Node));
	if (p == NULL) { exit(1); }
	p->data = data; p->next = NULL;
	if (head == NULL) {
		head = p;
	} else if (p->data <= head->data) {
		p->next = head; head = p;
	} else {
		ptr1 = head; ptr = head->next;
		//@ ghost j = 1;
		/*@ loop invariant //分成插在表中和表尾两情况。依指在链表中的指针，对链表分段描述。
			1 <= j <= m && oldhead == head && sorted_seg(head, ptr1) 
			&& \list_seg(head, ptr1) && ptr1 == head->(next:j-1)
			&& \list(p) && \length(p, next) == 1 && ptr1->data < p->data && p->data == data
			&& (	ptr != \null && ptr == ptr1->next && ptr1->data <= ptr->data
					&& sorted_list(ptr) && \length(ptr, next) == m - j 
				||
				ptr == \null && ptr1->next == \null && j == m
			    )
			;
		*/
		while ((ptr != NULL) && (ptr->data < p->data)) {
			ptr1 = ptr; ptr = ptr->next;
			//@ ghost j = j + 1;
		}
		p->next = ptr1->next; ptr1->next = p;
	}
	return head;
}
							图8.11 有序单向链表的插入函数		
		

　　形状标注 出现的地方可以概述如下。
　　（1）用于构造易变数据结构节点的类型声明中的各个指针都需要有标注，除非它作为静态区指针使用。
　　（2）对于拟指向堆块的声明指针

• 若从它的类型信息可清楚地知道它指向何种易变数据结构，则不用标注。
• 若从它的类型信息不知道它用于指向易变数据结构，则需要对它使用形状标注。
• 若从它的类型信息知道它指向何种易变数据结构，但缺少进一步信息（例如，指向主形状还是附加单向链表），则需要用形状标注指明细节，例如《安全C语言使用手册》例3.13的 additional_list。
• 不是用于指向堆块的指针，不能标注。

// 例8.8　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
//@	ghost bool allVisited; 
/*@	requires hTree(T);
	assigns allVisited;
	ensures hTree(T) && allVisited;
*/
void InOrderTraverse(const Node * const T) {  // T 指向头节点，头节点的l 链指向根节点 p
	//@ ghost Node *visited, *pred1, *pred2, *succ1, *succ2;
	p = T->l;
	//@	visited = T; allVisited = true;	// 先默认所有节点都能访问
	//@	ghost pred1 = T; pred2 = T; succ1 = T; succ2 = T; 
	/*@	loop invariant tTreeSeg(T->l, pred1, succ1, p, pred2, succ2) &&
			tTree(p, pred2, succ2) && visited == leftMost(p)->l && allVisited;
	*/
	while (p != T) {
		/*@	loop invariant tTreeSeg(T->l, pred1, succ1, p, pred2, succ2) &&
				tTree(p, pred2, succ2) && visited == leftMost(p)->l && allVisited;
		*/
		while(p->l_tag == Link) {
			//@ ghost succ2 = p;
			p = p->l;
		}
		// 访问节点p
		/*@	ghost 
			if (p->l_tag == Thread && visited == p->l ) {	// 上次访问的是它的前驱
				visited = p;	// 把p 记为上次访问的节点
			} else {
				allVisited = false; visited = p;			// 出现未按序访问，allVisited 置为false
			}
		*/
		/*@	loop invariant tTreeSeg(T->l, pred1, succ1, p, pred2, succ2) &&
				tTree(p, pred2, succ2) && visited == p && allVisited;
		*/
		while(p->r_tag == Thread && p->r != T) {
			//@ ghost pred2 = p;
			p = p->r; 
			// 访问节点p
			/*@ ghost
				if (p->r_tag == Thread && visited->r == p) {	// 同上
					visited = p;
				} else {
					allVisited = false; visited = p;
				}
			*/
		}
		//@ ghost pred2 = p;
		p = p->r;
	}
	return;
}
						图8.12 中序遍历访问线索二叉树节点的函数

　　幽灵变量（ghost variable）可以作为赋值的对象，这样的赋值不能出现在程序的可执行代码中，但可以出现在程序标注中对幽灵变量赋值的幽灵语句里。幽灵语句好像被执行而实际并不执行。好像被执行的意思是指，在程序验证时认为幽灵语句是程序的一部分，而在程序执行时这样的语句不存在。显然，幽灵语句不能对任何程序变量赋值，以保证不会改变基于程序变量能观察到的程序行为。
　　引入幽灵变量和幽灵语句是为了便于写程序规范。例如，遍历单向链表的循环以节点的 next 指针是否等于 NULL 来判断循环是否该终止了，并不需要有用来记住循环迭代计算次数的程序变量。但是没有这种记住循环迭代计算次数的变量，有时写不出循环不变式或者有这种记住迭代次数的变量会使得循环不变式容易写或直观易理解 。这时可以用幽灵变量及对其赋值的幽灵语句来记住循环迭代次数。

9.1 幽灵代码的语法

9.2 对幽灵代码的限制

9.3 幽灵变量和逻辑变量的区别

　　幽灵变量和幽灵语句 类似于C的变量和语句，但是仅在规范中可见。它们由出现在标注开头的关键字 ghost 引入，以 /*@ 开始并以 */ 结束，或者以 //@ 开始到本行结束。标注不能嵌套，单行的标注有完整的含义，不能改写成多行。幽灵变量和语句的文法见图9.1，但略去单行标注的文法没有给出。各产生式右部的终结符（ghost 除外）和非终结符都是ISO标准的C语言文法的终结符和非终结符，其中非终结符的文法没有任何SCSL扩展。该文法表明，幽灵变量和语句可以出现在C相应部分可出现的位置，只是须出现在标注中。

1. 出现在幽灵代码中的注释也必须以 // 开头并到其所在行的结尾结束，与第2章介绍词法时所说的一致。因为幽灵代码本身出现在C注释 /*@ … */ 中或 //@ 之后到所在行的结束，不是这样可能导致不正确的C代码。
2. 逻辑类型，例如 integer 和 real，也可以使用在幽灵代码中。
3. 关于幽灵函数、变量和域名的作用域，可以这么解释：把它们当成程序的一部分，按安全C语言的作用域规则来确定它们的作用域。
4. 非幽灵函数可以有幽灵形参。如果幽灵形参表子句出现在非幽灵函数声明的形参表之后，那么幽灵形参表必须非空，并且形参个数固定。该函数的调用者必须提供同样个数的幽灵形参。
5. 任何C代码的 if 语句，若它没有非幽灵的 else 子句，则可以用幽灵 else 子句来扩大。类似地，非幽灵 switch 语句可以用幽灵 default 开启的子句来扩大，如果原来不存在非幽灵 default 子句的话。非幽灵 switch 语句可以用幽灵 case 开启的子句来扩大。
6. 幽灵数组在某些方面与程序数组不同而与逻辑数组类似。首先，幽灵数组的声明有两种方式，指定大小和未指定大小的数组，后者可接受元素类型相同的任意大小的数组对它的赋值。幽灵数组的名字不被看成幽灵数组首元素的指针。

　　对于幽灵代码来说，语义上要求幽灵语句不改变程序的执行，因此，需要如下一些限制。

1. 幽灵代码不能修改任何非幽灵变量。
2. 幽灵代码不能修改任何结构体的非幽灵域。
3. 对于一个幽灵数组，区间赋值把一个数组分成一个或多个不相交区间。区间赋值只对幽灵数组的这些区间赋值。
4. 如果幽灵指针 p 指向非幽灵的内存单元，则 p 必须伴有 const 修饰符，用以表明不能不能通过 p 来修改非幽灵的内存单元。不允许出现指向堆易变数据结构的幽灵指针。
5. 幽灵函数的函数体是幽灵代码，不允许它修改任何非幽灵的变量和域。
6. 如果非幽灵的C函数被幽灵代码调用，则函数不能修改任何非幽灵的变量和域，还不能出现动态存储分配和释放。
7. 函数的控制流图不因幽灵语句而改变。具体说，不允许幽灵的 return、abort、exit 或 _exit 出现在非幽灵的C函数的函数体中，幽灵的 goto、break 和 continue 只能跳到幽灵代码，并且不能跳出包围该幽灵语句的最内非幽灵程序块。

// 例9.1
void f(int x, int *q) {
	//@ ghost int *p = q; 
	//@ ghost *p = 0; 	// The assignment is wrong: it modifies *q which lies in regular memory heap.
	//@ ghost p = &x;
	//@ ghost *p = 0; 	//The assignment is wrong: it modifies x which lies in regular memory stack.
}
							图9.2 非法的幽灵指针赋值语句

// 例9.2　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
int f(int x, int y) {
	//@ ghost int z = x + y;
	switch(x) {
		case 0: return y;
		//@ ghost case 1: z = y; break; // The statement is correct.
		//@ ghost case 2: { z++; break;}  // Invalid, would bypass the non-ghost default.
		default: y++;
	}
	return y;
}
int g(int x) {
	//@ ghost int z = x;
	if (x > 0) {return x;}
	//@ ghost else { z++; return x;} // Invalid, would bypass the non-ghost return.
	return x + 1;
}
					图9.3 非法的幽灵控制流语句

// 例9.3　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <stdio.h>	// 为简洁起见，本例没有给出检查输入和输出数据是否溢出的标注。
//@	ghost long input, output;
/*@	assigns input, output;
	ensures \result == 0 && output == 2 * input || \result == 1 && output == 0;
*/
int main() {
	long x;
	//@ ghost output = 0;
	if( scanf("%ld", &x) != 1 ) return 1;  // scanf函数需要检查返回值，读取失败时做出错处理
	//@ ghost input = x;
	printf("%ld\n", 2*x);
	//@ ghost output = 2*x;
	return 0;
}
						图9.4 利用幽灵变量的一个简单例子

// 例9.4　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
#include <limits.h>
//@ ghost int maxForbidden = 0;	
//@ global invariant M: 0 <= maxForbidden <= INT_MAX; // 变量不变式
/*@	assigns maxForbidden;
	ensures \result == maxForbidden;
*/
int gen() {
	static int x = 0;
	//@ global invariant I: 0 <= x <= INT_MAX;  // 变量不变式
	if (x != INT_MAX) x++;  // 防止数值计算溢出
	//@ ghost maxForbidden = x;
	return x;
}
						图9.5 利用幽灵变量的另 一个 简单例子

// 例9.5
#define LEN 1000
typedef int array[LEN];
/*@	predicate permutOne(array t1, array t2) =
		(\exists integer i:[0..\length(t1) -1], integer j:[0..\length(t1) -1]. i < j &&
			(\forall integer k:[0..i-1].t1[k] == t2[k]) && (\forall integer k:[i+1..j-1].t1[k] == t2[k]) &&
			(\forall integer k:[j+1..\length(t1)-1].t1[k] == t2[k]) && t1[i] == t2[j] && t1[j] == t2[i]);
	inductive permutAny(array t1, array t2, int n) =
		n == 0 && (\forall integer i:[0..\length(t1) -1].t1[i] == t2[i]) ||
		n == 1 && permutOne(t1, t2) ||
		n > 1 && (\exists array t3.permutAny(t1, t3, n-1) && permutOne(t3, t2)); 
*/
/*@	ghost array tempa; */
/*@	logic array olda;  */
/*@	requires olda[0..LEN-1] == a[0..LEN-1] && \length(a) == LEN;	
	assigns tempa, a[0..LEN-1];
	ensures (\forall integer i:[0..LEN-2]. a[i] <= a[i+1]) && (\exists integer n. n >= 0 &&
	permutAny(olda, a, n)) && \length(a) == LEN;  
*/
void bubbleSort(int* const a) {
	int low, up, j, k, temp;   /*@ ghost int n; */   
	low = 0; up = LEN-1; k = up;
	/*@	lemma permutAny_trans: \forall integer n.
		  n >= 1 && permutAny(olda, tempa, n-1) && permutOne(tempa, a) ==> permutAny(olda, a, n); */
	//@	ghost n = 0;
	/*@	loop invariant
		low == 0 && up == LEN-1 && k == up && \length(a) == LEN && 0 == n &&
			(\forall integer i:[k+1..up-1].a[i] <= a[i+1]) && permutAny(olda, a, 0) ||
		low == 0 && up == LEN-1 && low <= k < up && \length(a) == LEN && 0 <= n &&
			(\forall integer i : [low..k]. a[i] <= a[k+1]) &&
			(\forall integer i : [k+1..up-1]. a[i] <= a[i+1]) && permutAny(olda, a, n); 
	*/
	while(k != low) {
		j = low;
		/*@	loop invariant
		  low == 0 && up == LEN-1 && k == up && low <= j <= k && \length(a) == LEN && 0 == n &&
			  (\forall integer i : [low..j-1]. a[i] <= a[j]) && (\forall integer i : [k+1..up-1]. a[i] <= a[i+1]) &&
				permutAny(olda, a, n) ||
		  low == 0 && up == LEN-1 && k == up &&  low <= j <= k && \length(a) == LEN && 0 < n &&
			  (\forall integer i : [low..j-1]. a[i] <= a[j]) && (\forall integer i : [k+1..up-1]. a[i] <= a[i+1]) &&
				permutAny(olda, a, n) ||
		  low == 0 && up == LEN-1 && low < k < up && low <= j <= k && \length(a) == LEN && 0 <= n &&
			  (\forall integer i : [low..j-1]. a[i] <= a[j]) &&(\forall integer i : [low..k]. a[i] <= a[k+1]) &&
				(\forall integer i : [k+1..up-1]. a[i] <= a[i+1]) && 
				permutAny(olda, a, n); 
		*/
		while(j != k) {
			if (a[j] > a[j+1]) { 
				//@ ghost tempa[0..LEN-1] = a[0..LEN-1]; 
				temp = a[j]; a[j] = a[j+1]; a[j+1] = temp; 
				//@ ghost n = n + 1; 
			}
			j = j + 1;
		}
		k = k -1;
	}
	return;
}
								图9.6 冒泡排序函数的代码和标注

// 例9.6
typedef enum {BLUE, WHITE, RED} color;
/*@	logic int numof(color* t, int n, color c) = (n <= 0) ? 0 : ((t[n-1] == c? 1 : 0) + numof(t, n-1, c));
	predicate permut(color* t1, color* t2, int n) =
		\length(t1) == n && \offset(t1) == 0 && \length(t2) == n && \offset(t2) == 0 && n > 0 &&
		numof(t1, n, RED) == numof(t2, n, RED) && numof(t1, n, WHITE) == numof(t2, n, WHITE) &&
		numof(t1, n, BLUE) == numof(t2, n, BLUE);  
*/
//@	ghost color tmpColors[];
/*@	requires 0 <= i <= j && \length(t) > j && \forall int k:[0..\length(t)-1].tmpColors[k] == t[k];
	assigns t[i], t[j];
	ensures t[i] == tmpColors[j] && t[j] == tmpColors[i] &&(\forall int k:[0..i-1].tmpColors[k] == t[k]) &&
	      (\forall int k:[i+1..j-1].tmpColors[k] == t[k])&&(\forall int k:[j+1..\length(t)-1].tmpColors[k] == t[k]);
*/
void swap(color* const t, int const i, int const j){
	color tmp;
	tmp = t[i];  t[i] = t[j];  t[j] = tmp;
}

#define N 100
typedef struct flag{int n; color* colors;}flag;
//@ strong type invariant is_colored(flag f) = 0 < f.n <= N && \length(f.colors)==f.n && \offset(f.colors)==0;
//@ predicate isMonochrome(color* t, int i, int j, color c) = \forall int k:[i..j]. t[k] == c;
//@ logic flag oldf;
/*@ requires oldf == f;
	assigns tmpColors[0..f.n-1], f.colors[0..f.n-1];
	ensures (\exists int b:[0..f.n]. \exists int r:[0..f.n].
		b <= r && isMonochrome(f.colors, 0, b-1, BLUE) && isMonochrome(f.colors, b, r-1, WHITE) &&
		isMonochrome(f.colors, r, f.n-1, RED) && permut(oldf.colors, f.colors, f.n));
*/
void dutchFlag(const flag f){
	int b = 0, i = 0; int r; color* t; color tmp;
	/*@	lemma counting: (\forall int i:[0..f.n-1].tmpColors[i] == f.colors[i])
	==>	numof(tmpColors, f.n, RED) == numof(f.colors, f.n, RED) && numof(tmpColors, f.n, WHITE) ==
		numof(f.colors, f.n, WHITE) && numof(tmpColors, f.n, BLUE) == numof(f.colors, f.n, BLUE); 
	*/
	t = f.colors;  r = f.n;
	//@ ghost tmpColors[0..f.n-1] = f.colors[0..f.n-1];
	/*@ loop invariant
		0 <= b <= i <= r <= f.n && oldf == f && \length(t) == f.n && \offset(t) == 0 && t == f.colors &&
		isMonochrome(f.colors, 0, b-1, BLUE) && isMonochrome(f.colors, b, i-1, WHITE) &&
		isMonochrome(f.colors, r, f.n-1, RED) &&
		permut(oldf.colors, tmpColors, f.n) && tmpColors[0..f.n-1] == f.colors[0..f.n-1];
	*/
	while(i < r) {
		switch (t[i]) {
			case BLUE: swap(t, b, i); b = b+1; i = i+1; break;
			case WHITE: i = i+1; break;
			case RED: r = r-1; swap(t, i, r); break;
		}
		//@ ghost tmpColors[0..f.n- 1] = f.colors[0..f.n-1];
	}
}

							图9.7 Dijkstra 荷兰国旗算法的代码和标注

#define N 100
int count(int* a){  // 统计长度为N的数组a中值为0的元素个数
	int k, j;
	k = 0;
	for(j = 0; j < N; j = j + 1){	
	    if(a[j] == 0){
	        k = k+1;
	    }
	}
	return k;
}

#define N 100
/*@ ghost  // 幽灵函数定义的开始
    /@ requires \length(a) == N && \offset(a) == 0;	
       ensures 0 <= \result <= N;  					
    @/  // 幽灵函数协议的范围标记为 /@ 和 @/。注意，这里不是标注的嵌套
    int count(int* a){
	int k, j;
	k = 0;

	/@ loop invariant \length(a) == N && \offset(a) == 0 &&
		0 <= k <= j && 0 <= j <= N; 
	@/ // 循环不变式的前后也用 /@ 和 @/ 做标记
	for(j = 0; j < N; j = j + 1){
	    if(a[j] == 0){
	        k = k+1;
	    }
	}

	return k;
    }
*/  // 幽灵函数定义的结束

1. 和幽灵语句一样，幽灵函数的标注一定以 /*@ ghost 开始，一直到该标注的结束。
2. 幽灵函数的函数协议和函数中的循环不变式、循环变式都以 /@ 开始并且都以 @/ 结束。 因为标注不能嵌套，/@ ... @/ 是对幽灵函数内的标注（如函数协议等）进行特殊处理的提示。非幽灵函数中的幽灵循环语句的循环不变式、循环变式也按此方式处理。 其它标注中若出现 /@ ... @/，将被作为非法字符，不会被按此方式处理。
3. 在幽灵函数中，对幽灵语句的限制同本节开头提到的那几点是一致的。
4. 幽灵函数用于帮助收集程序点的状态能满足的断言，一般来说不会复杂，毕竟它不能破坏当前程序状态。

　　幽灵变量和逻辑变量一致之处是，它们都是为了方便写程序规范而引入的，它们都不能被程序访问。但是它们是有区别的，因而不能相互取代。逻辑变量仅可以出现在断言中，用于表达程序代码（主要是函数对上下文的不变性质。而幽灵变量出现在程序标注里面的幽灵语句中，在幽灵语句中可以对幽灵变量赋值。幽灵语句好像被执行而实际并不执行。幽灵变量用于帮助表达 函数代码本身的性质，因而幽灵变量也可以出现在断言中。

• 幽灵变量的优点是，可以通过对幽灵变量的赋值，记住程序变量在某个程序点的值。逻辑变量做不到这一点。
• 使用逻辑变量的场合，也可以通过给函数增加带const限定的幽灵参数而取代逻辑变量。这么做的缺点是对被验证函数增加的标注较多，没有逻辑变量方式直观。
• 幽灵变量的声明可以出现在头文件中。与逻辑变量不同的是，包含该头文件的各个源文件认定该幽灵变量代表同一个幽灵对象。

　　为方便对使用库函数的程序的验证，我们根据库函数的功能和使用中所关心的性质，为一些常用的库函数添加了函数协议。下面给出的是相应的库函数的名字和函数协议。

• 1.1 逻辑定义
  //@ logic integer oldc_ctype;


• 1.2 isalnum
  

  /*@ requires -1<=is_c<=255 && \old(is_c) == is_c ;
      ensures
          (48 <= \old(is_c) <= 57 || 65 <= \old(is_c) <= 90 || 97 <= \old(is_c) <= 122) && \result != 0
          ||
          (-1 <= \old(is_c) <= 47 || 58 <= \old(is_c) <= 64 || 91 <= \old(is_c) <= 96 || 123 <= \old(is_c) <= 255) 
          && \result == 0
          ;
  */

  extern int isalnum (int is_c); // 检查字符is_c是否是字母和数字


• 1.3 isalpha
  

  /*@ requires -1<=is_c<=255 && is_c == \old(is_c);
      ensures
  	(65 <= \old(is_c) <= 90 || 97 <= \old(is_c) <= 122)
  	&& \result != 0
  	||
  	(-1 <= \old(is_c) <= 64 || 91 <= \old(is_c) <= 96 || 123 <= \old(is_c) <= 255)
  	&& \result == 0
  	;
  */

  extern int isalpha (int is_c); // 检查字符is_c是否是字母


• 1.4 isascii
  

  /*@ requires -1<=__c<=255 && \old(__c) == __c;
      ensures
  	0 <= \old(__c) <= 127 && \result != 0  
  	||
  	(\old(__c) == -1 || 128 <= \old(__c) <= 255) && \result == 0
  	;
  */

  extern int isascii (int __c);


• 1.5 isblank
  

  /*@ requires -1<=is_c<=255 && is_c == \old(is_c);
      ensures
  	(\old(is_c) == 9 || \old(is_c) == 32) && \result != 0
  	||
  	(-1 <= \old(is_c) < =8 || 10 <= \old(is_c )< =31 || 33 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isblank (int is_c);


• 1.6 iscntrl
  

  /*@ requires -1<=is_c<=255 && is_c == \old(is_c);
  ensures
  	(0 <= \old(is_c) <= 31 || \old(is_c) == 127) && \result != 0
  	||
  	(\old(is_c) == -1 || 32 <= \old(is_c) <= 126 || 128 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int iscntrl (int is_c); // 检查字符is_c是否是控制字符


• 1.7 isdigit
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures 
  	48 <= \old(is_c) <= 57 && \result != 0
  	||
  	(-1 <= \old(is_c) <= 47 || 58 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isdigit (int is_c); // 检查字符is_c是否是十进制数字


• 1.8 islower
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures
  	97 <= \old(is_c) <= 122 && \result != 0
  	|| 
  	(-1 <= \old(is_c) <= 96 || 123 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int islower (int is_c); // 检查字符is_c是否是小写字母


• 1.9 isgraph
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures
  	33 <= \old(is_c) <= 126 && \result != 0
  	||
  	(-1 <= \old(is_c) <= 32 || 127 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isgraph (int is_c); // 检查字符is_c是否有图形表示法


• 1.10 isprint
  

  /*@ requires -1<=is_c<=255 && is_c == \old(is_c);
      ensures
  	32 <= \old(is_c )<= 126 && \result != 0
  	||
  	(-1 <= \old(is_c) <= 31 || 127 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isprint (int is_c); // 检查字符is_c是否是可打印的


• 1.11 ispunct
  

  /*@ requires -1 < =is_c<=255 && is_c == \old(is_c);
      ensures
  	(33 <= \old(is_c) <= 47 || 58 <= \old(is_c) <= 64 || 91 <= \old(is_c) <= 96 || 123 <= \old(is_c) <= 126) && \result != 0
  	||
  	(-1 <= \old(is_c) <= 32 || 48 <= \old(is_c) <= 57 || 65 <= \old(is_c) <= 90 || 97 <= \old(is_c) <= 122 || 127 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int ispunct (int is_c); // 检查字符is_c是否是标点符号字符


• 1.12 isspace
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures
  	(9 <= \old(is_c) <= 13 || \old(is_c)==32) && \result != 0
  	||
  	(-1 <= \old(is_c) <= 8 || 14 <= \old(is_c) <= 31 || 33 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isspace (int is_c); // 检查字符is_c是否是空白字符


• 1.13 isupper
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures
  	65 <= \old(is_c) <= 90 && \result != 0
  	||
  	(-1 <= \old(is_c) <= 64 || 91 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isupper (int is_c); // 检查字符is_c是否是大写字母


• 1.14 isxdigit
  

  /*@ requires -1 <= is_c <= 255 && is_c == \old(is_c);
      ensures
  	(48 <= \old(is_c) <= 57 || 65 <= \old(is_c) <= 70 || 97 <= \old(is_c) <= 102) && \result != 0
  	||
  	(-1 <= \old(is_c) <= 47 || 58 <= \old(is_c) < =64 || 71 <= \old(is_c) <= 96 || 103 <= \old(is_c) <= 255) && \result == 0
  	;
  */

  extern int isxdigit (int is_c); // 检查字符is_c是否是十六进制数字


• 1.15 tolower
  

  /*@ requires -1<=__c<=255 && \old(__c) == __c;
      ensures
  	65 <= \old(__c) <= 90 && \result == \old(__c)+32
  	||
  	(-1 <= \old(__c) <= 64 || 91 <= \old(__c) <= 255) && \result == \old(__c)
  	;
  */

  extern int tolower (int __c); // 把给定的字母__c转换为小写字母


• 1.16 toupper
  

  /*@ requires -1<=__c<=255 && \old(__c) == __c;
      ensures
  	97 <= \old(__c) <= 122 && \result == \old(__c)-32
  	||
  	(-1 <= \old(__c) <= 96 || 123 <= \old(__c) <= 255) && \result == \old(__c)
  	;
  */

  extern int toupper (int __c); // 把给定的字母__c转换为大写字母

• 2.1 逻辑定义
  //@ logic char *olddest_string, *oldsrc_string, *p1_string, *p2_string;
  //@ logic integer m_string, n_string, k_string, oldn_string, oldch_string, oldstr_length;
  //@ logic char *strstr_oldfind,*strstr_oldneed;
  


• 2.2 strcpy
  

  /*@ requires
          \is_pstring(__src, \strlen(__src)) && m_string == \strlen(__src)
          && \length(__dest) - \offset(__dest) > \strlen(__src)
          && olddest_string == __dest
          && \old(__src) == __src
          && \offset(__dest) >= 0 && \offset(__src) >= 0
          && \old(olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]) == olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]
          ;
      assigns olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1];
      ensures
          \result == olddest_string
          && \offset(olddest_string) >= 0
          && \offset(\old(__src)) >= 0
          && \length(olddest_string) - \offset(olddest_string) > m_string
          && \is_pstring(\result, m_string)
          && \is_pstring(\old(__src), m_string)
          && \string(\result, m_string) == \string(\old(__src), m_string)
          && olddest_string[m_string+1..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[m_string+1..\length(olddest_string)-\offset(olddest_string)-1])
          ;
  */

  extern char *strcpy (char *__restrict __dest, const char *__restrict __src); // 把 src 所指向的字符串复制到 dest


• 2.3 strncpy
  

  /*@ requires
          \is_pstring(__src, \strlen(__src)) && m_string == \strlen(__src)
          && __dest == olddest_string
          && __src == \old(__src)
          && __n == oldn_string
          && \length(__dest) - \offset(__dest) > oldn_string
          && \offset(__dest) >= 0
          && \offset(__src) >= 0
          && 0 <= oldn_string
          && \old(olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]) == olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]
          ;
      assigns olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1];
      ensures
          \result == olddest_string
          && \is_pstring(\old(__src), m_string)
          && \offset(olddest_string) >= 0
          && \offset(\old(__src)) >= 0
          && \length(olddest_string) - \offset(olddest_string) > oldn_string
          && (
              oldn_string > m_string
              && \is_pstring(olddest_string ,m_string)
              && \string(olddest_string ,m_string) == \string(\old(__src),m_string)
              && olddest_string[m_string+1..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[m_string+1..\length(olddest_string)-\offset(olddest_string)-1])
              ||
              0 <= oldn_string <= m_string
              && \is_string(olddest_string , oldn_string)
              && \string(olddest_string ,oldn_string) == \string(\old(__src),oldn_string)
              && olddest_string[oldn_string..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[oldn_string..\length(olddest_string)-\offset(olddest_string)-1])
              )
          ;
  */

  extern char *strncpy (char *__restrict __dest, const char *__restrict __src, size_t __n);
  // 把 src 所指向的字符串复制到 dest，最多复制 n 个字符。当 src 的长度小于 n 时，dest 的剩余部分将用空字节填充。


• 2.4 strcat
  

  /*@ requires
          \is_pstring(__dest, \strlen(__dest)) && m_string == \strlen(__dest)
          && \is_pstring(__src, \strlen(__src)) && n_string == \strlen(__src)
          && __dest == olddest_string
          && __src == \old(__src)
          && \strlen(__dest) + \strlen(__src) < \length(__dest) - \offset(__dest)
          && \offset(__src) >= 0
          && \offset(__dest) >= 0
          && \old(olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]) == olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]
          ;
      assigns olddest_string[m_string..\length(olddest_string)-\offset(olddest_string)-1];
      ensures
          \is_pstring(\result, m_string + n_string)
          && \is_pstring(\old(__src), n_string)
          && m_string + n_string < \length(olddest_string) - \offset(olddest_string)
          && \result == olddest_string
          && \offset(olddest_string) >= 0
          && \offset(\old(__src)) >= 0
          && \string(olddest_string,m_string + n_string) == \string(olddest_string,m_string) + \string(\old(__src),n_string) //使用谓词描述新的字符串
          && olddest_string[m_string+n_string+1..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[m_string+n_string+1..\length(olddest_string)-\offset(olddest_string)-1])
          ;
  */

  extern char *strcat (char * __restrict __dest, const char * __restrict __src);
  // 把 src 所指向的字符串追加到 dest 所指向的字符串的结尾


• 2.5 strncat
  

  /*@ requires
          \is_pstring(__dest, \strlen(__dest)) && m_string == \strlen(__dest)
          && \is_pstring(__src, \strlen(__src)) && n_string == \strlen(__src)
          && __dest == olddest_string
          && __src == \old(__src)
          && __n == oldn_string
          && oldn_string >= 0
          && \strlen(__dest) + \strlen(__src) < \length(__dest) - \offset(__dest)
          && \offset(__dest) >= 0
          && \offset(__src) >= 0
          && \old(olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]) == olddest_string[0..\length(olddest_string)-\offset(olddest_string)-1]
          ;
      assigns olddest_string[m_string..\length(olddest_string)-\offset(olddest_string)-1];
      ensures
          \is_pstring(\old(__src), n_string)
          && \result == olddest_string
          && oldn_string >= 0
          && \offset(olddest_string) >= 0
          && \offset(\old(__src)) >= 0
          && m_string + n_string < \length(olddest_string) - \offset(olddest_string)
          &&  (
                  oldn_string <= n_string
                  && \is_pstring(olddest_string, m_string + oldn_string)
                  && \string(olddest_string,m_string + oldn_string) == \string(olddest_string,m_string) + \string(\old(__src),oldn_string)
                  && olddest_string[m_string+oldn_string+1..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[m_string+oldn_string+1..\length(olddest_string)-\offset(olddest_string)-1])
                ||
                  oldn_string > n_string
                  && \is_pstring(olddest_string, m_string + n_string)
                  && \string(olddest_string,m_string + n_string) == \string(olddest_string,m_string) + \string(\old(__src),n_string)
                  && olddest_string[m_string+n_string+1..\length(olddest_string)-\offset(olddest_string)-1] == \old(olddest_string[m_string+n_string+1..\length(olddest_string)-\offset(olddest_string)-1])
              )
          ;
  */

  extern char *strncat (char *__restrict __dest, const char *__restrict __src,size_t __n);
  // 把 src 所指向的字符串追加到 dest 所指向的字符串的结尾，直到 n 字符长度为止


• 2.6 strcmp
  

  /*@ requires
          \is_pstring(__s1, \strlen(__s1))
          && \is_pstring(__s2, \strlen(__s2))
          && __s1 == \old(__s1)
          && __s2 == \old(__s2)
          && \offset(__s1) >= 0
          && \offset(__s2) >= 0
          ;
      ensures
          \is_pstring(\old(__s1), \strlen(\old(__s1)))
          && \is_pstring(\old(__s2), \strlen(\old(__s2)))
          && \offset(\old(__s1)) >= 0
          && \offset(\old(__s2)) >= 0
          && (
               \string(\old(__s1), \strlen(\old(__s1))) < \string(\old(__s2), \strlen(\old(__s2))) && \result < 0
             ||
               \string(\old(__s1), \strlen(\old(__s1))) == \string(\old(__s2), \strlen(\old(__s2))) && \result == 0
             ||
               \string(\old(__s1), \strlen(\old(__s1))) > \string(\old(__s2), \strlen(\old(__s2))) && \result > 0
             )
          ;
  */

  extern int strcmp (const char *__s1, const char *__s2); // 把 str1 所指向的字符串和 str2 所指向的字符串进行比较


• 2.7 strncmp
  

  /*@ requires
          \is_pstring(__s1, \strlen(__s1))
          && \is_pstring(__s2, \strlen(__s2))
          && __n >= 0
          && __s1 == \old(__s1)
          && __s2 == \old(__s2)
          && __n == \old(__n)
          && \offset(__s1) >= 0
          && \offset(__s2) >= 0
          ;
      ensures
          \is_pstring(\old(__s1), \strlen(\old(__s1)))
          && \is_string(\old(__s2), \strlen(\old(__s2)))
          && \offset(\old(__s1)) >= 0
          && \offset(\old(__s2)) >= 0
          &&(
              \result < 0
              &&(
                    \strlen(\old(__s1)) >= \old(__n)
                    && \strlen(\old(__s2)) >= \old(__n)
                    && \prefix(\string(\old(__s1), \strlen(\old(__s1))), \old(__n)) < \prefix(\string(\old(__s2), \strlen(\old(__s2))), \old(__n))
                  ||
                    (\strlen(\old(__s1)) < \old(__n) || \strlen(\old(__s2)) < \old(__n))
                    && \string(\old(__s1), \strlen(\old(__s1))) < \string(\old(__s2), \strlen(\old(__s2)))
                )
              ||
                \result == 0 &&
                      (\strlen(\old(__s1)) >= \old(__n) && \strlen(\old(__s2)) >= \old(__n) && \prefix(\string(\old(__s1), \strlen(\old(__s1))), \old(__n)) == \prefix(\string(\old(__s2), \strlen(\old(__s2))), \old(__n))
                      || \strlen(\old(__s1)) < \old(__n) && \strlen(\old(__s2)) == \strlen(\old(__s1)) && \string(\old(__s1), \strlen(\old(__s1))) == \string(\old(__s2), \strlen(\old(__s2))))
              || \result > 0 &&
                      (\strlen(\old(__s1)) >= \old(__n) && \strlen(\old(__s2)) >= \old(__n) && \prefix(\string(\old(__s1), \strlen(\old(__s1))), \old(__n)) > \prefix(\string(\old(__s2), \strlen(\old(__s2))), \old(__n))
                      || (\strlen(\old(__s1)) < \old(__n) || \strlen(\old(__s2)) < \old(__n)) && \string(\old(__s1), \strlen(\old(__s1))) > \string(\old(__s2), \strlen(\old(__s2))))
              )
          ;
  */

  extern int strncmp (const char *__s1, const char *__s2, size_t __n); // 把 str1 和 str2 进行比较，最多比较前 n 个字节


• 2.8 strcoll
  

  /*@ requires
          \is_pstring(__s1, \strlen(__s1))
          && \is_pstring(__s2, \strlen(__s2))
          && \old(__s1) == __s1
          && \old(__s2) == __s2
          && \offset(__s1) >= 0
          && \offset(__s2) >= 0
          ;
      ensures
          \is_pstring(\old(__s1), \strlen(\old(__s1)))
          && \is_pstring(\old(__s2), \strlen(\old(__s2)))
          && \offset(\old(__s1)) >= 0
          && \offset(\old(__s2)) >= 0
          &&
            (  \string(\old(__s1), \strlen(\old(__s1))) < \string(\old(__s2), \strlen(\old(__s2))) && \result < 0
             ||
               \string(\old(__s1), \strlen(\old(__s1))) == \string(\old(__s2), \strlen(\old(__s2))) && \result == 0
             ||
               \string(\old(__s1), \strlen(\old(__s1))) > \string(\old(__s2), \strlen(\old(__s2))) && \result > 0
            )
          ;
  */

  extern int strcoll (const char *__s1, const char *__s2);
  // 把 str1 和 str2 进行比较，结果取决于 LC_COLLATE 的位置设置


• 2.9 strchr
  

  /*@ requires
          \is_pstring(__s, \strlen(__s)) && 0 <= __c <= 255
          && __s == \old(__s)
          && __c == \old(__c)
          && \offset(__s) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \strlen(\old(__s))) && \result == \null && \offset(\old(__s)) >= 0 && \length(\old(__s)) >= 0
          && !\membership(\string(\old(__s), \strlen(\old(__s))), \old(__c))
        ||
          \is_pstring(\old(__s), \strlen(\old(__s))) && \offset(\old(__s)) >= 0 && \length(\old(__s)) >= 0
          && 0 <= \offset(\result)-\offset(\old(__s)) < \strlen(\old(__s))
          && *(\result) == \old(__c) && \offset(\old(__s)) >= 0
          && \result == \old(__s) + \offset(\result) - \offset(\old(__s))  // 需要这个断言，表明\result和\old(__s)指向同一个数据块
          && !\membership(\prefix(\string(\old(__s), \strlen(\old(__s))), \offset(\result) - \offset(\old(__s))), \old(__c))
          ;
  */

  extern char *strchr (const char *__s, int __c) __THROW __attribute_pure__ __nonnull ((1));
  // 在参数 str 所指向的字符串中搜索第一次出现字符 c（一个无符号字符）的位置


• 2.10 strrchr
  

  /*@ requires
          \is_pstring(__s, \strlen(__s))
          && 0 <= __c <=255
          && __s == \old(__s)
          && __c == \old(__c)
          && \offset(__s) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \strlen(\old(__s))) && \result == \null
          && !\membership(\string(\old(__s), \strlen(\old(__s))), \old(__c))
          && \offset(\old(__s)) >= 0
        ||
          \is_pstring(\old(__s), \strlen(\old(__s)))
          && 0 <= \offset(\result)-\offset(\old(__s)) < \strlen(\old(__s))
          && *(\result) == \old(__c)
          && \offset(\old(__s)) >= 0
          && \result == \old(__s) + \offset(\result) - \offset(\old(__s)) // 需要这个断言，表明\result和\old(__s)指向同一个数据块
          && !\membership(\suffix(\string(\old(__s), \strlen(\old(__s))), \strlen(\old(__s)) - (\offset(\result) - \offset(\old(__s)) +1)), \old(__c))
          ;
  */

  extern char *strrchr (const char *__s, int __c)__THROW __attribute_pure__ __nonnull ((1));
  // 在参数 str 所指向的字符串中搜索最后一次出现字符 c（一个无符号字符）的位置


• 2.11 strcspn
  

  /*@ requires
          \is_pstring(__s, \strlen(__s))
          && \is_pstring(__reject, \strlen(__reject))
          && __s == \old(__s)
          && __reject == \old(__reject)
          && \offset(__s) >= 0
          && \offset(__reject) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \strlen(\old(__s)))
          && \offset(\old(__s)) >= 0
          && \offset(\old(__reject)) >= 0
          && \is_pstring(\old(__reject), \strlen(\old(__reject)))
          && (\forall integer i:[0..\result-1].!\membership(\string(\old(__reject), \strlen(\old(__reject))), \old(__s)[i]))
          && (
                  0 <= \result < \strlen(\old(__s)) && \membership(\string(\old(__reject), \strlen(\old(__reject))), \old(__s)[\result])
              ||
                  \result == \strlen(\old(__s))
              )
          ;
  */

  extern size_t strcspn (const char *__s, const char *__reject) __THROW __attribute_pure__ __nonnull ((1, 2));
  // 检索字符串 str1 开头连续有几个字符都不含字符串 str2 中的字符


• 2.12 strspn
  

  /*@ requires
          \is_pstring(__s, \strlen(__s))
          && \is_pstring(__accept, \strlen(__accept))
          && \old(__s) == __s
          && \old(__accept) == __accept
          && \offset(__s) >= 0
          && \offset(__accept) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \strlen(\old(__s)))
          && \is_pstring(\old(__accept), \strlen(\old(__accept)))
          && \offset(\old(__s)) >= 0
          && \offset(\old(__accept)) >= 0
          && (\forall integer i:[0..\result-1].\membership(\string(\old(__accept), \strlen(\old(__accept))),\old(__s)[i]))
          && (
                  0 <= \result < \strlen(\old(__s))
                  && !\membership(\string(\old(__accept), \strlen(\old(__accept))), \old(__s)[\result])
                ||
                  \result == \strlen(\old(__s))
             )
          ;
  */

  extern size_t strspn (const char *__s, const char *__accept); // 检索字符串 str1 中第一个不在字符串 str2 中出现的字符下标


• 2.13 strpbrk
  

  /*@ requires
          \is_pstring(__s, \strlen(__s))
          && \is_pstring(__accept, \strlen(__accept))
          && __s == \old(__s)
          && __accept == \old(__accept)
          && \offset(__s) >= 0
          && \offset(__accept) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \strlen(\old(__s)))
          && \is_pstring(\old(__accept), \strlen(\old(__accept))) && \offset(\old(__s)) >= 0 && \offset(\old(__accept)) >= 0
          &&  (
                \result == \null
                && (\forall integer i:[0..\strlen(\old(__s))-1].!\membership(\string(\old(__accept), \strlen(\old(__accept))), \old(__s)[i]))
              ||
                0 <= \offset(\result)-\offset(\old(__s)) <= \strlen(\old(__s))
                && \result == \old(__s) + \offset(\result)-\offset(\old(__s))
                && (
                      \forall integer i:[0..\offset(\result)-\offset(\old(__s))-1].!\membership(\string(\old(__accept), \strlen(\old(__accept))), \old(__s)[i]))
                      && \membership(\string(\old(__accept), \strlen(\old(__accept))),\result[0])
              )
          ;
  */

  extern char *strpbrk (const char *__s, const char *__accept);
  // 检索字符串 str1 中第一个匹配字符串 str2 中字符的字符，不包含空结束字符。
  // 也就是说，依次检验字符串 str1 中的字符，当被检验字符在字符串 str2 中也包含时，则停止检验，并返回该字符位置。


• 2.14 strstr
  

  /*@ requires
          \is_pstring(__haystack, \strlen(__haystack))
          && \is_pstring(__needle, \strlen(__needle))
          && \strlen(__haystack) > 0
          && \strlen(__needle) > 0
          && __haystack == \old(__haystack)
          && __needle == \old(__needle)
          && \offset(__haystack) >= 0
          && \offset(__needle) >= 0
          ;
      ensures
          \is_pstring(\old(__haystack), \strlen(\old(__haystack))) && \offset(\old(__haystack)) >= 0
          && \is_pstring(\old(__needle), \strlen(\old(__needle))) && \offset(\old(__needle)) >= 0
          && (
                \result == \null
                && !\contains(\string(\old(__haystack), \strlen(\old(__haystack))),\string(\old(__needle), \strlen(\old(__needle))))
              ||
                \result == \old(__haystack) + \offset(\result) - \offset(\old(__haystack))
                && 0 <= \offset(\result) - \offset(\old(__haystack)) <= \strlen(\old(__haystack)) - \strlen(\old(__needle))
                && \is_pstring(\result,\strlen(\old(__haystack))-\offset(\result)+\offset(\old(__haystack)))
                && (\forall integer i:[0..\strlen(\old(__needle))-1].
                    \old(__haystack)[\offset(\result) - \offset(\old(__haystack)) + i] == \old(__needle)[i])
                && (\forall integer i:[0..\offset(\result)-\offset(\old(__haystack)) - 1].
                    \exists integer j:[0..\strlen(\old(__needle))-1].\old(__haystack)[i+j] != \old(__needle)[j])
             )
          ;
  */

  extern char *strstr (const char *__haystack, const char *__needle);
  // 在字符串 haystack 中查找第一次出现字符串 needle 的位置，不包含终止符 '\0'。


• 2.15 strlen
  

  /*@ requires
          \is_pstring(__s,\strlen(__s))
          && \old(__s) == __s
          && \offset(__s) >= 0
          ;
      ensures
          \is_pstring(\old(__s), \result)
          && \result == \strlen(\old(__s))
          && \offset(\old(__s)) >= 0
          ;
  */

  extern size_t strlen (const char *__s); // 计算字符串 str 的长度，直到空结束字符，但不包括空结束字符。

• 3.1 逻辑定义与不变式
  //@ logic FILE *oldstream;
  //@ logic char *oldmode_stdio;
  //@ logic char *oldbuf_stdio;
  //@ logic integer intmode_stdio;
  //@ logic integer old_flag_stdio;
  //@ logic integer oldoffset_stdio;
  //@ logic integer oldwhence_stdio;
  //@ logic integer oldc_stdio;
  //@ logic integer oldsize_stdio;
  //@ logic integer oldn_stdio;
  //@ logic integer oldnmemb_stdio;
  //@ logic char *olds_stdio;
  //@ logic char *oldptr;
  //@ logic size_t oldsize;
  
  
• 3.2 fclose
  

  /*@ requires 
  	__stream != \null && \old(__stream) == __stream;
      assigns 
  	*\old(__stream);
      ensures  
  	(   \result == 0 && \old(__stream)->_flags == 0 
  	  || 
  	    \result == EOF
  	)
  	;
  */

  extern int fclose (FILE *__stream); // 关闭文件流 stream，刷新所有的缓冲区


• 3.3 fopen
  

  /*@ requires 
  	\is_pstring(__filename,\strlen(__filename)) 
  	&& oldmode_stdio == __modes 
  	&& 
  	(
  		( \is_pstring(__modes,1) 
  			&& ( \string(__modes, 1) == "r" || \string(__modes, 1) == "w" || \string(__modes, 1) == "a" )
  		) 
  	||
  		( \is_pstring(__modes,2) 
  			&&  (  \string(__modes, 2) == "rb" || \string(__modes, 2) == "wb" || \string(__modes, 2) == "ab" 
  				|| \string(__modes, 2) == "r+" || \string(__modes, 2) == "w+" || \string(__modes, 2) == "a+" 
  				)
  		) 
  	||
  		( \is_pstring(__modes,3) 
  			&&  (  \string(__modes, 3) == "rb+" || \string(__modes, 3) == "wb+" || \string(__modes, 3) == "ab+" 
  				|| \string(__modes, 3) == "r+b" || \string(__modes, 3) == "w+b" || \string(__modes, 3) == "a+b" 
  				)
  		)
  	);
  
      ensures  
  	\result == \null 
  	|| 
  	\result != \null && \length(\result) == 1 && \offset(\result) == 0
  	&&  (
  		(\is_pstring(oldmode_stdio,1) 
  		&&  (  \string(oldmode_stdio, 1) == "r" && \result->_flags == -72539000
  			|| \string(oldmode_stdio, 1) == "w" && \result->_flags == -72539004
  			|| \string(oldmode_stdio, 1) == "a" && \result->_flags == -72534908
  			)
  		) 
  		||
  		(\is_pstring(oldmode_stdio,2) 
  		&&  (  \string(oldmode_stdio, 2) == "rb" && \result->_flags == -72539000
  			|| \string(oldmode_stdio, 2) == "wb" && \result->_flags == -72539004
  			|| \string(oldmode_stdio, 2) == "ab" && \result->_flags == -72534908
  			|| \string(oldmode_stdio, 2) == "r+" && \result->_flags == -72539008
  			|| \string(oldmode_stdio, 2) == "w+" && \result->_flags == -72539008
  			|| \string(oldmode_stdio, 2) == "a+" && \result->_flags == -72534912
  			)
  		) 
  		||
  		(\is_pstring(oldmode_stdio,3) 
  		&&  (  \string(oldmode_stdio, 3) == "rb+" && \result->_flags == -72539008
  			|| \string(oldmode_stdio, 3) == "wb+" && \result->_flags == -72539008 
  			|| \string(oldmode_stdio, 3) == "ab+" && \result->_flags == -72534912
  			|| \string(oldmode_stdio, 3) == "r+b" && \result->_flags == -72539008 
  			|| \string(oldmode_stdio, 3) == "w+b" && \result->_flags == -72539008 
  			|| \string(oldmode_stdio, 3) == "a+b" && \result->_flags == -72534912
  			)
  		)
  	)
  	;
  */
  

  extern FILE *fopen (const char *__restrict __filename, const char *__restrict __modes) __wur;
  // 使用给定的模式 mode 打开 filename 所指向的文件。


• 3.4 setbuf
  

  /*@ requires  
  	oldstream == __stream == \old(__stream)
  	&& oldstream->_flags == \old(oldstream->_flags)
  	;
      assigns
  	*\old(__stream);
      ensures 
  	oldstream->_flags == \old(oldstream->_flags) + 1
  	;
  */

  extern void setbuf (FILE *__restrict __stream, char *__restrict __buf) __THROW; // 定义流 stream 应如何缓冲。
  // 该函数应在与流 stream 相关的文件被打开时，且还未发生任何输入或输出操作之前被调用一次。


• 3.5 fgetc
  

  /*@ requires 
          __stream != \null 
          && \old(__stream) == __stream == oldstream
          && \old(*oldstream) == *oldstream
          && ((oldstream->_flags & _IO_NO_WRITES) == 0 || (oldstream->_flags & _IO_NO_WRITES) != 0)
          ;		 
      assigns *\old(__stream);
      ensures 
          oldstream != \null 
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES) 
          && (
              \result >= 0 && \result <=127
              && (\old(*oldstream)._flags & _IO_NO_READS) == 0 
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
            || 
              \result == EOF 
              && (
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      && (\old(*oldstream)._flags & _IO_NO_READS) != 0 
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0  
                 ) 
             )  
          ;
  */

  extern int fgetc (FILE * __stream);
  // 从指定的流 stream 获取下一个字符（一个无符号字符），并把位置标识符往前移动。


• 3.6 getc
  

  /*@ requires 
          __stream != \null 
          && \old(__stream) == __stream == oldstream
          && \old(*oldstream) == *oldstream
          && ((oldstream->_flags & _IO_NO_WRITES) == 0 || (oldstream->_flags & _IO_NO_WRITES) != 0)
          ;
      assigns *\old(__stream);
      ensures 
          oldstream != \null		
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES) 
          &&(
              \result >= 0 && \result <= 127
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
              && (\old(*oldstream)._flags & _IO_NO_READS) == 0 
              
            || 
              \result == EOF 
              &&(
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      && (\old(*oldstream)._flags & _IO_NO_READS) != 0 
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0 
                ) 
            )
          ;
  */

  extern int getc (FILE *__stream); // 从指定的流 stream 获取下一个（无符号）字符，并把位置标识符往前移动。


• 3.7 fputc
  

  /*@ requires 
          __stream != \null && oldstream == __stream == \old(__stream)
          && __c >= 0 && __c <= 127 
          && __c == \old(__c)
          && \old(*oldstream) == *oldstream
          && ((oldstream->_flags & _IO_NO_READS) == 0 || (oldstream->_flags & _IO_NO_READS) != 0)
          ;
      assigns *\old(__stream);
      ensures 
          oldstream != \null  
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES) 
          && (oldstream->_flags & _IO_CURRENTLY_PUTTING) != 0 
          && (
              \result == \old(__c) 
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
              && (oldstream->_flags & _IO_NO_WRITES) == 0 
              || 
                \result == EOF 
                &&(
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      && (\old(*oldstream)._flags & _IO_NO_WRITES) != 0
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0 
                  )
             )
          ;
  */

  extern int fputc (int __c, FILE * __stream);
  // 把参数 char 指定的字符（一个无符号字符）写入到指定的流 stream 中，并把位置标识符往前移动。


• 3.8 putc
  

  /*@ requires 
          __stream != \null && oldstream == __stream == \old(__stream)
          && __c >= 0 && __c <= 127 
          && __c == \old(__c)
          && \old(*oldstream) == *oldstream
          && ((oldstream->_flags & _IO_NO_READS) == 0 || (oldstream->_flags & _IO_NO_READS) != 0)
          ;
      assigns *\old(__stream);
      ensures 
          oldstream != \null  
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES) 
          && (oldstream->_flags & _IO_CURRENTLY_PUTTING) != 0 
          && 
            (
              \result == \old(__c) 
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
              && (oldstream->_flags & _IO_NO_WRITES) == 0 
              || 
                \result == EOF 
                &&(
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      && (\old(*oldstream)._flags & _IO_NO_WRITES) != 0
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0 
                  )
            )
          ;
  */

  extern int putc (int __c, FILE *__stream);
  // 把参数 char 指定的字符（一个无符号字符）写入到指定的流 stream 中，并把位置标识符往前移动。


• 3.9 fgets
  

  /*@ requires 
          __stream != \null 
          && oldstream == __stream == \old(__stream) 
          && __n >= 1 && \length(__s) >= __n && \offset(__s) >= 0
          && olds_stdio == __s == \old(__s) 
          && __n  == \old(__n)
          && \old(*oldstream) == *oldstream
          && \old(olds_stdio[0..\length(olds_stdio) - \offset(olds_stdio) - 1]) == olds_stdio[0..\length(olds_stdio) - \offset(olds_stdio) - 1]
          ;
      assigns *\old(__stream),\old(__s)[0..\length(\old(__s)) - \offset(\old(__s)) - 1];
      ensures   
          oldstream != \null 
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES)
          && (	
              \is_pstring(\result, \strlen(\result)) 
              && (\forall integer i:[0..\strlen(\result)-1].0 <= olds_stdio[i] <= 127) 
              && \is_pstring(olds_stdio,\strlen(olds_stdio)) 
              && olds_stdio[\strlen(\result)..\length(olds_stdio) - \offset(olds_stdio) - 1] == \old(olds_stdio[\strlen(\result)..\length(olds_stdio) - \offset(olds_stdio) - 1])
              && \strlen(\result) <= \old(__n)              //fgets只能读取一行
              && \strlen(olds_stdio) <= \old(__n)     
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
              && (\old(*oldstream)._flags & _IO_NO_READS) == 0 
            || 
              \result == \null 
              &&(
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      && (\old(*oldstream)._flags & _IO_NO_READS) != 0  
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0 
                )
             )
          ;
  */

  extern char *fgets (char *__restrict __s, int __n, FILE *__restrict __stream);
  // 从指定的流 stream 读取一行，并把它存储在 str 所指向的字符串内。
  // 当读取 (n-1) 个字符时，或者读取到换行符时，或者到达文件末尾时，它会停止，具体视情况而定。
  


• 3.10 fputs
  

  /*@ requires 
          __stream != \null 
          && oldstream == __stream == \old(__stream)
          && \is_pstring(__s,\strlen(__s)) 
          && olds_stdio == __s 
          && \old(*oldstream) == *oldstream
          && ((oldstream->_flags & _IO_NO_READS) == 0 || (oldstream->_flags & _IO_NO_READS) != 0)
          ;
      assigns *\old(__stream);
      ensures  
          oldstream != \null 
          && \is_pstring(olds_stdio,\strlen(olds_stdio))
          && (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES) 
          && (oldstream->_flags & _IO_CURRENTLY_PUTTING) != 0 
          && (
              \result >= 0 
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0 
              && (\old(*oldstream)._flags & _IO_NO_WRITES) == 0 
            || 
              \result == EOF 
              &&(
                  (oldstream->_flags & _IO_ERR_SEEN) != 0
                    && (\old(*oldstream)._flags & _IO_NO_WRITES) != 0 
                  || 
                  (oldstream->_flags & _IO_EOF_SEEN) != 0 
                )
             )
          ;
  */

  extern int fputs (const char *__restrict __s, FILE *__restrict __stream);
  // 把字符串写入到指定的流 stream 中，但不包括空字符。


• 3.11 fread
  

  /*@  requires 
          __stream != \null 
          && __n == \old(__n)
          && oldsize == __size == \old(__size)
          && oldstream == __stream == \old(__stream)
          &&  __ptr == \old(__ptr)
          && __n >= 0 && __size >= 0 
          && \length(__ptr) >= __size*__n 
          && \old(*oldstream) == *oldstream
          && (\typeof(*__ptr) == char || \typeof(*__ptr) == int)
          ;
      assigns *\old(__stream); 
      ensures  
          (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES)
          && (
              oldsize != 0 
              && \old(__n) != 0 
              && (
                  \result == \old(__n) 
                  && (oldstream->_flags & _IO_ERR_SEEN) == 0 
                  && (oldstream->_flags & _IO_EOF_SEEN) == 0   
                 || 
                  0 < \result < \old(__n) 
                  &&(
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                    || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0
                    )
                 )
                  && (\old(*oldstream)._flags & _IO_NO_READS) == 0 
                || 
                  \result == 0 
                  && (
                      \old(__size) == 0 
                      || 
                      \old(__n) == 0 
                      || 
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                          && (\old(*oldstream)._flags & _IO_NO_READS) != 0 
                      || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0)
              )
          ;
  */

  extern size_t fread (void *__restrict __ptr, size_t __size, size_t __n, FILE *__restrict __stream) __wur;
  // 从给定流 stream 读取数据到 ptr 所指向的数组中。


• 3.12 fwrite
  

  /*@  requires 
          __s != \null 
  		&& __n == \old(__n)
  		&& __size == \old(__size)
  		&& oldstream == __s == \old(__s)
  		&& __n >= 0 
  		&& __size >= 0 
  		&& \length(__ptr) >= __size*__n 
  		&& \old(*oldstream) == *oldstream
  		&& (\typeof(*__ptr) == char || \typeof(*__ptr) == int)
  		;
  	assigns *\old(__s);
      ensures  
  		(\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
  		&& (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES)
  		&&  (	
  				(	
  					(\old(*oldstream)._flags & _IO_NO_WRITES) == 0 
  					&& \old(__size) != 0 
  					&& \old(__n) != 0 
  					&& (oldstream->_flags & _IO_CURRENTLY_PUTTING) != 0 
  					&&  (
  							\result == \old(__n) 
  							&& (oldstream->_flags & _IO_ERR_SEEN) == 0 
  							&& (oldstream->_flags & _IO_EOF_SEEN) == 0 
  						  || 
  							0 < \result < \old(__n) 
  							&& (oldstream->_flags & _IO_ERR_SEEN) != 0
  						)
  				) 
  			  || 
  				\result == 0 
  				&&(	
  					\old(__size) == 0 || \old(__n) == 0 && (\old(*oldstream)._flags & _IO_NO_WRITES) != 0 
  					|| 
  					(oldstream->_flags & _IO_ERR_SEEN) != 0
  				  )
  			)
  		;
  */

  extern size_t fwrite (const void *__restrict __ptr, size_t __size, size_t __n, FILE *__restrict __s);
  // 把 ptr 所指向的数组中的数据写入到给定流 stream 中。


• 3.13 fseek
  

  /*@ requires 
          oldstream == __stream  == \old(__stream)
          && \old(__off) == __off 
          && __whence == \old(__whence)
          && oldstream->_flags != 0 
          && \old(*oldstream) == *oldstream
          && (__whence == SEEK_SET || __whence == SEEK_CUR || __whence == SEEK_END)
          ;
      assigns *\old(__stream);       
      ensures 
          (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS) 
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES)
          && (
              (
                  \result == -1 
                  &&  (
                      (oldstream->_flags & _IO_ERR_SEEN) != 0 
                      || 
                      (oldstream->_flags & _IO_EOF_SEEN) != 0
                      )
              )
              ||
                  \result == 0 
                  && (oldstream->_flags & _IO_ERR_SEEN) == 0 
                  && (oldstream->_flags & _IO_EOF_SEEN) == 0
             )
          ;
  */

  extern int fseek (FILE *__stream, long int __off, int __whence);
  // 设置流 stream 的文件位置为给定的偏移 offset，参数 offset 意味着从给定的 whence 位置查找的字节数。


• 3.14 ftell
  

  /*@	requires 
          oldstream == __stream  == \old(__stream)
          && \old(*oldstream) == *oldstream
          ;
      assigns *\old(__stream);
      ensures 
          (\old(*oldstream)._flags & _IO_NO_READS) == (oldstream->_flags & _IO_NO_READS)             
          && (\old(*oldstream)._flags & _IO_NO_WRITES) == (oldstream->_flags & _IO_NO_WRITES)
          &&	(
              \result == -1 
              &&  (
                  (oldstream->_flags & _IO_ERR_SEEN) != 0 
                  || 
                  (oldstream->_flags & _IO_EOF_SEEN) != 0
                  )
              )
              ||
              \result >= 0 
              && (oldstream->_flags & _IO_ERR_SEEN) == 0 
              && (oldstream->_flags & _IO_EOF_SEEN) == 0
          ;
  */

  extern long int ftell (FILE *__stream) __wur; // 返回给定流 stream 的当前文件位置


• 3.15 rewind
  

  /*@ requires 
  	oldstream == __stream  == \old(__stream) && __stream != \null;
      assigns
  	*\old(__stream);
      ensures 
  	oldstream->_offset == 0;
  */

  extern void rewind (FILE *__stream); // 设置文件位置为给定流 stream 的文件的开头


• 3.16 feof
  

  /*@ requires 
  	oldstream == __stream && __stream != \null;
      ensures  
  	\result == (oldstream->_flags & _IO_EOF_SEEN);
  */

  extern int feof (FILE *__stream) __THROW __wur; // 测试给定流 stream 的文件结束标识符


• 3.17 ferror
  

  /*@ requires 
  	oldstream == __stream && __stream != \null;
      ensures  
  	\result == (oldstream->_flags & _IO_ERR_SEEN);
  */

  extern int ferror (FILE *__stream) __THROW __wur; // 测试给定流 stream 的错误标识符


• 3.18 freopen
  

  /*@ requires 
          \is_pstring(__filename,\strlen(__filename)) 
          && oldmode_stdio == __modes 
          && \length(__stream) >= 1
          && \offset(__stream) >= 0
          && (( \is_pstring(__modes,1) 
                && ( \string(__modes, 1) == "r" || \string(__modes, 1) == "w" || \string(__modes, 1) == "a" )
              ) 
              ||
              ( \is_pstring(__modes,2) 
                && ( \string(__modes, 2) == "rb" || \string(__modes, 2) == "wb" ||
                     \string(__modes, 2) == "ab" || \string(__modes, 2) == "r+" || 
                     \string(__modes, 2) == "w+" || \string(__modes, 2) == "a+"  )
              ) 
              ||
              ( \is_pstring(__modes,3) 
                && ( \string(__modes, 3) == "rb+" || \string(__modes, 3) == "wb+" || 
                     \string(__modes, 3) == "ab+" || \string(__modes, 3) == "r+b" || 
                     \string(__modes, 3) == "w+b" || \string(__modes, 3) == "a+b"  )
              )
             );
      ensures  
          \result == \null 
          || 
          \result != \null && \length(\result) == 1 && \offset(\result) == 0
          && ((\is_pstring(oldmode_stdio,1) 
               && (  \string(oldmode_stdio, 1) == "r" && \result->_flags == -72539000
                   ||\string(oldmode_stdio, 1) == "w" && \result->_flags == -72539004
                   ||\string(oldmode_stdio, 1) == "a" && \result->_flags == -72534908 )
              ) 
              ||
              (\is_pstring(oldmode_stdio,2) 
               && (  \string(oldmode_stdio, 2) == "rb" && \result->_flags == -72539000
                   ||\string(oldmode_stdio, 2) == "wb" && \result->_flags == -72539004
                   ||\string(oldmode_stdio, 2) == "ab" && \result->_flags == -72534908
                   ||\string(oldmode_stdio, 2) == "r+" && \result->_flags == -72539008
                   ||\string(oldmode_stdio, 2) == "w+" && \result->_flags == -72539008
                   ||\string(oldmode_stdio, 2) == "a+" && \result->_flags == -72534912)
              ) 
              ||
              (\is_pstring(oldmode_stdio,3) 
               && (  \string(oldmode_stdio, 3) == "rb+" && \result->_flags == -72539008
                   ||\string(oldmode_stdio, 3) == "wb+" && \result->_flags == -72539008 
                   ||\string(oldmode_stdio, 3) == "ab+" && \result->_flags == -72534912
                   ||\string(oldmode_stdio, 3) == "r+b" && \result->_flags == -72539008 
                   ||\string(oldmode_stdio, 3) == "w+b" && \result->_flags == -72539008 
                   ||\string(oldmode_stdio, 3) == "a+b" && \result->_flags == -72534912)
              )
          )
          ;
  */

  extern FILE *freopen (const char *__restrict __filename, const char *__restrict __modes, FILE *__restrict __stream) __wur;
  // 将一个新的文件名 __filename 与给定的打开的流 __stream 关联，同时关闭流中的旧文件。


• 3.19 标准输入输出流的强变量不变式
  extern struct _IO_FILE *stdin;　　　/* Standard input stream. */
  //@ strong global invariant stdlen1_len : \length(stdin) == 1;
  extern struct _IO_FILE *stdout;　　/* Standard output stream. */
  //@ strong global invariant stdlen2_len : \length(stdout) == 1;
  extern struct _IO_FILE *stderr;　　/* Standard error output stream. */
  //@ strong global invariant stdlen3_len : \length(stderr) == 1;
  

　　对于一些常用、但SCSL目前尚不支持，无法给出函数协议的库函数，如函数的参数个数可变的 printf、scanf, 实参类型可变的快排函数qsort等。系统为此类库函数提供了内部支持，使程序员可以在程序中使用它们。
　　这类库函数和相应函数协议描述如下，如果函数调用时满足其前件的要求，函数执行结束后就能获得其后件的性质。

• 1. free
  

  /*@ requires \singleton(p);
      ensures  \dangling(p);
  */

  void free(void* const p);


• 2. exit
  

  /*@ ensures \false;
      exist   \exit_status = status;
  */

  void exit(const int status);


• 3. malloc
  

  /*@ requires size > 0;
      ensures  \result == \null || \singleton(\result);
  */

  void* malloc(size_t size);


• 4. calloc
  

  /*@ requires size > 0 && n > 0;
      ensures  \result == \null ||
               \singleton(\result) && \length(\result) == n && \offset(\result) == 0;
  */

  void* calloc(size_t n, size_t size);


• 5. scanf
  

  /*@ assigns arg1, arg2,..., argn;
      ensures \result == -1 ||
              \result == 0 ||
              \result == 1 && arg1 相关断言: \is_pstring(arg1,\strlen(arg1))、0<= arg1 <= 999 等 ||
              \result == 2 && arg1、arg2 相关断言 ||
              ...
              \result == n && arg1、arg2、...、argn 相关断言;
  */

  int scanf(const char *format, ...);


• 6. printf
  

  /*@ ensures \true;*/

  int printf(const char *format, ...);


• 7. sscanf
  

  /*@ assigns arg1, arg2,..., argn;
      ensures \result == -1 ||
              \result == 0 ||
              \result == 1 && arg1相关断言: \is_pstring(arg1,\strlen(arg1))、0<=arg1<=999等 ||
              \result == 2 && arg1、arg2相关断言 ||
              ...
              \result == n && arg1、arg2、...、argn相关断言;
  */

  int sscanf(const char *str, const char *format, ...); // str相关断言请见相应头文件的协议


• 8. sprintf
  

  /*@ ensures \true;*/

  int sprintf(char *str, const char *format, ...); // str相关断言请见相应头文件的协议


• 9. memcpy
  

  /*@ requires \typeof(dest) == type && \typeof(src) == type && \length(dest)-\offset(dest) >=n && 
  	     \length(src)-\offset(src) >= n;
      assigns  dest[0..n-1];
      ensures  \result == dest && \typeof(dest) == type && \forall int i:[0..n-1].dest[i] == src[i];
  */

  void * memcpy(void* dest, const void* src, size_t n);


• 10. memcmp
  

  /*@ requires \typeof(dest) == type && \typeof(src) == type && 
  	     \length(dest)-\offset(dest) >= size/sizeof(type) && \length(src)-\offset(src) >= size/sizeof(type);
      ensures  \result == 0 && \forall int i:[0..size/sizeof(type)-1].dest[i] == src[i] ||
  			0 <= !k && !k < size/sizeof(type) && (\forall int i:[0..!k-1].dest[i] == src[i]) &&
  			(dest[!k] < src[!k] && \result < 0 || dest[!k] > src[!k] && \result > 0);
  */

  int memcmp(const void* dest, const void* src, size_t size);


• 11. memset
  

  /*@ requires \typeof(s) == type && \length(s)-\offset(s) >= size/sizeof(type);
      assigns  dest[0..size/sizeof(type)-1];
      ensures  \result == s && \typeof(s) == type && 
  	     \forall int i:[0..size/sizeof(type)-1]."s[i] == c" // 这里的 == 是指每个字节等于 c & 0xff;
  */
  

  void *memset (void* s, int c, size_t size);


• 12. free
  

  /*@ requires \typeof(dest) == type && \typeof(src) == type && 
  	     \length(dest)-\offset(dest) >= n && \length(src)-\offset(src) >= n;
      assigns  dest[0..n-1], src[0..n-1];
      ensures  \result == dest && \typeof(dest) == type && \forall int i:[0..n-1].dest[i] == \old(src[i]);
  */

  void* memmove(void* dest, const void* src, size_t n);


• 13. qsort
  

  /*@ requires \length(p) == len && size == \sizeof(*p) && \typeof(*p) == type && 
  	     \forall int i:[0..len-1].\forall int j:[0..len-1].compare_pre[p+i/q,p+j/t];
      assigns  p[0..len-1];
      ensures  \forall int i:[0..len-2]. !k <= 0 && compare_post[!k/\result];
  */

  void qsort(void* p, size_t len, size_t size, int (*compare)(const void* q, const void* t));
  // 详细请参见《安全C规范语言使用手册》4.8