ACSL 及Frama-C验证工具简介（一）

ACSL 及相关工具简介

在软件系统的开发过程中，如何检查功能模块是否符合设计预期并保证这些模块能够正确的组合在一起实现更复杂的功能，是一个核心问题。测试（testing）的方法在一定程度上能够帮助我们发现一些问题；但要获得更可靠的保证，往往需要借助程序验证（verification）的方法：亦即使用某种形式化的语言（通常包括了对谓词逻辑的支持）对程序行为作出规范，然后使用逻辑规则证明相关代码符合给出的规范。

由法国原子能和替代能源委员会下属实验室（CEA-LIST）和法国国家信息与自动化研究所（INRIA）主导的“ANSI/ISO C 规范语言”（the ANSI/ISO C Specification Language，简称 ACSL）就是这样一种适用于 C 语言的行为接口规范语言（Behavioral Interface Specification Language，BISL）。它以特殊注释的格式穿插在 C 代码之中，精确严谨地刻画相关代码片段、乃至整个函数的行为和性质。一些自动化验证工具，例如 frama-c，能够解析经 ACSL 标注的 C 代码，用静态分析的方法自动验证其是否严格遵守了规范的约束。

ACSL 的实用性不仅仅体现在它拥有 frama-c 这样的自动证明工具，也体现在它允许灵活的模块化的规范书写。例如，每个功能模块/函数可以对应一组规范，亦即函数合约；只要可以证明某模块满足其合约，它的调用者就可以直接信赖合约中约定的性质，进而（结合其它子功能模块）实现更复杂的功能，而无需了解各个子模块的具体实现。

下文中我们将先简单介绍 ACSL 及其使用场景，然后从应用的角度出发ÿ