名称：acsl-annotation-assistant 描述：为C/C++程序创建ACSL（ANSI/ISO C Specification Language）形式注释。在形式验证、添加函数契约（requires/ensures）、循环不变量、断言、内存安全注释或任何ACSL规范时使用此技能。支持Frama-C验证，并为C/C++代码生成全面的形式规范。版本：1.0.0 标签：

验证
frama-c
acsl
c-verification 难度：中级语言：
c
acsl 依赖：
hoare-logic-verifier

ACSL注释助手

为C/C++程序生成全面的ACSL（ANSI/ISO C Specification Language）注释，以支持使用工具如Frama-C进行形式验证。

核心能力

1. 函数契约

添加完整的函数规范，包括前置条件和后置条件：

/*@
  requires \valid(array + (0..n-1));
  requires n > 0;
  ensures \result >= 0 && \result < n;
  ensures \forall integer i; 0 <= i < n ==> array[\result] >= array[i];
  assigns 
othing;
*/
int find_max_index(int *array, int n);

2. 循环注释

生成循环不变量、变体和assigns子句：

/*@
  loop invariant 0 <= i <= n;
  loop invariant \forall integer k; 0 <= k < i ==> sum == \sum(0, k, array);
  loop assigns i, sum;
  loop variant n - i;
*/
for (i = 0; i < n; i++) {
    sum += array[i];
}

3. 内存安全规范

添加指针有效性和分离注释：

/*@
  requires \valid(dest + (0..n-1));
  requires \valid_read(src + (0..n-1));
  requires \separated(dest + (0..n-1), src + (0..n-1));
  ensures \forall integer i; 0 <= i < n ==> dest[i] == \old(src[i]);
  assigns dest[0..n-1];
*/
void memcpy_safe(char *dest, const char *src, size_t n);

4. 断言和假设

插入运行时和验证断言：

//@ assert 0 <= index && index < array_length;
//@ assume divisor != 0;

5. 公理化定义和谓词

定义可重用的逻辑谓词和公理：

/*@
  predicate sorted{L}(int *a, integer n) =
    \forall integer i, j; 0 <= i <= j < n ==> a[i] <= a[j];
*/

/*@
  axiomatic Sum {
    logic integer sum{L}(int *a, integer low, integer high);

    axiom sum_empty{L}:
      \forall int *a, integer i; sum(a, i, i) == 0;

    axiom sum_next{L}:
      \forall int *a, integer low, high;
        low < high ==> sum(a, low, high) == sum(a, low, high-1) + a[high-1];
  }
*/

注释工作流程

步骤1：分析函数

在注释之前：

识别输入、输出和副作用
确定内存访问模式
理解算法属性（排序、搜索等）
注意任何隐含假设

步骤2：添加函数契约

从函数级规范开始：

前置条件 (requires)：函数调用时必须为真
后置条件 (ensures)：函数返回时将真
Assigns子句：可能修改的内存位置
行为规范：如果适用，正常和异常行为

步骤3：注释循环

对于每个循环，指定：

循环不变量：每次迭代前后都成立的属性
循环变体：证明终止的递减度量
循环assigns：循环内修改的内存

步骤4：添加断言

插入中间断言以：

文档化算法属性
帮助验证工具
澄清复杂逻辑

步骤5：定义辅助谓词

创建可重用的逻辑定义，用于：

常见模式（排序数组、有效范围）
领域特定属性
复杂数学关系

常见ACSL构造

内存有效性

\valid(ptr)                    // 单个有效指针
\valid(ptr + (low..high))      // 有效范围
\valid_read(ptr)               // 只读有效性
\separated(ptr1, ptr2)         // 无别名

量词

\forall type var; condition ==> property
\exists type var; condition && property

逻辑函数

\old(expr)                     // 函数入口时的值
\at(expr, Label)               // 特定点的值
\result                        // 函数返回值

othing                       // 空集（用于assigns）

整数范围

\forall integer i; low <= i < high ==> array[i] >= 0

行为

/*@
  behavior valid_input:
    assumes n > 0;
    requires \valid(array + (0..n-1));
    ensures \result >= 0;

  behavior invalid_input:
    assumes n <= 0;
    ensures \result == -1;

  complete behaviors;
  disjoint behaviors;
*/

验证考虑

对于Frama-C WP插件

当为WP验证生成注释时：

使用assigns子句指定框架条件
偏好\valid而不是原始指针检查
使用\separated表示指针分离
为所有循环添加loop assigns
包括loop variant以证明终止

常见验证模式

数组边界安全：

/*@ requires 0 <= index < length;
    requires \valid(array + index);
*/

空指针检查：

/*@ requires ptr != 
ull;
    requires \valid(ptr);
*/

溢出预防：

/*@ requires INT_MIN <= a + b <= INT_MAX; */

输出格式

以标准ACSL注释语法生成注释：

多行契约：/*@ ... */
单行断言：//@ assertion
将契约直接放在函数声明之前
将循环注释直接放在循环头部之前
当注释复杂时，包括解释性注释

最佳实践

从简单开始：先使用基本契约，然后细化
精确：避免过度规范或不足规范
文档化假设：使隐含假设显式化
使用谓词：提取常见模式
增量测试：使用Frama-C逐步验证注释
包括原理：添加注释解释非明显规范

示例：完整注释函数

/*@
  predicate valid_array(int *a, integer n) =
    \valid(a + (0..n-1)) && n > 0;
*/

/*@
  requires valid_array(array, n);
  ensures \result >= 0 && \result < n;
  ensures \forall integer i; 0 <= i < n ==> array[\result] >= array[i];
  assigns 
othing;
*/
int find_max_index(int *array, int n) {
    int max_idx = 0;

    /*@
      loop invariant 0 <= i <= n;
      loop invariant 0 <= max_idx < n;
      loop invariant \forall integer k; 0 <= k < i ==>
                     array[max_idx] >= array[k];
      loop assigns i, max_idx;
      loop variant n - i;
    */
    for (int i = 1; i < n; i++) {
        if (array[i] > array[max_idx]) {
            max_idx = i;
        }
    }

    return max_idx;
}

资源

此技能包括ACSL参考资料：

references/

acsl_reference.md - 全面的ACSL语法参考
common_patterns.md - 常用注释模式
frama_c_integration.md - 使用Frama-C的提示

根据需要加载这些参考资料以获取详细语法信息或高级模式。

研究工具与工件

现实世界中的ACSL和形式验证工具：

工具	为何重要
Frama-C	工业C验证平台
WP插件	C的演绎验证
Jessie	通过Why3的演绎验证
AST插件	抽象语法树分析
值分析	静态值范围分析
E-ACSL	运行时验证转换

关键验证项目

OpenSSL验证：证明加密原语正确性
Sel4微内核：OS内核正确性证明
CompCert：验证的C编译器

研究前沿

当前ACSL和C验证的活跃研究：

方向	关键论文	挑战
自动化	“自动不变量生成”（2019）	生成循环不变量
SMT理论	“C中的线性算术”（2020）	更好的算术支持
并发性	“并发分离逻辑”	验证多线程C
幽灵代码	“幽灵状态”（Iris）	丰富的规范逻辑
测试集成	“演绎测试”（2021）	结合测试和证明

实现陷阱

ACSL注释中常见错误：

陷阱	真实示例	预防
缺少assigns	Frama-C报告警告	始终指定变化
弱不变量	验证静默失败	使不变量足够强
缺少循环assigns	不完整框架	注释每个循环
溢出假设	算术中的不健全性	使用适当边界
分离违规	别名错误	显式使用\separated
不完整行为	错过错误情况	使用complete/disjoint行为

ACSL注释助手Skill acsl-annotation-assistant