c - C的Java建模语言？

Question

我记得不久前读过一些关于 C 的正式规范语言的内容，但现在我需要它却找不到它。

它受到 JML 的启发，就我所见使用相同的语法。

我发现它的唯一参考是一篇论文，但我所说的比这更精致。

如果这给你敲响了警钟……

如果没有人知道这一点，我会很高兴听到一种在 C 中进行形式验证和自动测试生成的方法。

提前致谢。

Answer 1

我对 CML 不熟悉，但是您链接的文章以声明它是用于规范非功能性需求的开头。

JML 是针对 Java 程序的功能需求的（好吧，界限很模糊，但我认为 CML 文章使用的这个词与这句话的含义相同）。用于 C 程序的 JML 的等价物（因此也纯粹用于功能需求）是ACSL。

对于形式验证，我只能推荐Frama-C（免责声明：我在 Frama-C 上工作，但与 ACSL 规范无关）。对于 C 程序的测试生成，我听说过CUTE的好消息。

Answer 2

“为”C 的正式规范？

我知道正式指定C: Denotational Semantics for C的工作。

如果您想指定C 程序做什么，那么属性规范语言可能是一个有用的起点。

Answer 3

C 周围至少有 4 个验证系统：

1. 埃舍尔 C 验证器。[我与此有关。]
2. 微软 VCC。
3. 带有 Jessie 插件的Frama-C（在软件包中的 Debian/Ubuntu 上可用frama-c。您why也需要安装才能使 jessie 工作）
4. 极速。

(1) 适用于以 MISRA-C 或类似语言编写的安全关键型嵌入式 C 程序。(2) 适用于使用 Microsoft C 编译器构建的多线程系统。我对 (3) 和 (4) 知之甚少。