ANSI/ISO C规范语言

ANSI/ISO C规范语言（ ACSL ）是使用合同范式设计的hoare样式前和后条件和不变性的C程序的规范语言。规格写为对C程序的C注释评论，因此可以与任何C编译器一起编译。

当前的ACSL验证工具是frama-c 。它还实现了针对C ++定义的姊妹语言， ANSI/ISO C ++规范语言（ ACSL ++ ）。

概述

1983年，美国国家标准研究所（ANSI）委托X3J11委员会标准化C语言。 C的第一个标准由ANSI发布。尽管该文件随后被国际标准化组织（ISO）采用，而ISO随后的修订已被ANSI采用，但仍将使用ANSI C的名称。

ACSL是一种行为接口规范语言（BISL）。它旨在指定C源代码的行为属性。该语言的主要灵感来自Caduceus工具的规范语言，用于扣除C程序的行为属性。 Caduceus的规范语言本身是由JML启发的，其旨在针对Java源代码的类似目标。

与JML的不同之处在于，ACSL旨在用于静态验证和演绎验证，而JML均设计用于运行时断言检查和使用例如ESC/Java工具的静态验证。

句法

考虑以下示例的函数的原型，名为incrstar ：

/*@ requires \valid(p);
  @ assigns *p;
  @ ensures *p == \old(*p) + 1;
  @*/
void incrstar (int *p);

合同由以/*@开头的评论给出。它的含义如下：

• 第一行是一个前提：它指出必须使用指向安全分配的内存位置的指针p调用功能incrstar 。
• 第二行是帧子句，指出功能incrstar不会修改任何内存位置，而是由p指向的位置。
• 最后， ensures条款是后条件，该条款指定值*p由一个递增。

上述功能的有效实现将是：

void incrstar (int *p) {
    (*p)++;
}

工具支持

ACSL的大多数功能都由Frama-C支持。

Trustinsoft静态分析仪是Frama-C的商业衍生产品。它验证程序行为，并（基于语言规范的内置规则）捕获不确定行为的实例。