C语言的Java建模语言？

Question

我记得在前一段时间阅读了有关C的正式规范语言的一些内容，但现在我找不到它，我需要它。

它的灵感来自于JML，只要我看到相同的语法。

我发现的唯一参考是一个paper，但是我所说的比这更好。

如果这听起来很耳熟你...

如果没有人知道这一点，我会很高兴听到办法做正式验证和自动测试代C.

谢谢提前。

Answer 1

我对CML并不熟悉，但链接的文章首先声明它是用于规定非功能性需求的。 JML是针对Java程序的功能需求（好的，这行很模糊，但我认为CML文章使用与这句话相同含义的词）。 C程序的JML的等价物（因此也仅限于功能要求）为ACSL。

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

Answer 2

Formal specification for“C？

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

如果你想指定什么 C程序做，那么Property Specification Language可能是一个有用的开始。

Answer 3

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

1. 埃舍尔Ç验证。 [我与此连接。]
2. Microsoft VCC。
3. Frama-C与杰西插件（在Debian/Ubuntu的可在包frama-c。您需要安装why太让杰西工作）
4. VeriFast。

（1）适用于使用MISRA-C或类似软件编写的安全至关重要的嵌入式C程序。 （2）适用于使用Microsoft C编译器构建的多线程系统。 我知道比较少（3）和（4）。