C 语言的 Java 建模语言？
我记得不久前读过一些关于 C 的形式化规范语言的内容，但现在我需要它却找不到它。
它受到 JML 的启发，据我所知使用相同的语法。
我发现的唯一参考是 论文，但我所说的比这更精致。
如果这给你敲响了警钟......
如果没有人知道这一点，我会很高兴听到一种用 C 进行形式验证和自动测试生成的方法。
提前致谢。
I remember reading something about a formal specification language for C a while ago, but I can not find it now that I need it.
It was inspired by JML, using as far as I saw the same syntax.
The only reference to it I found is a paper, but what I am talking about was more polished than that.
If this rings a bell to you...
If nobody knows about this, I'll be happy to hear about a way to do formal verification and automatic test generation in C.
Thanks in advance.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
我不熟悉 CML，但您链接的文章开头声明它用于非功能性需求的规范。
JML 是针对 Java 程序的功能需求（好吧，这条线很模糊，但我认为 CML 文章使用的这个词与这句话的含义相同）。 C 程序的 JML 的等价物（因此也纯粹是为了功能需求）是 ACSL。
对于形式验证，我只能推荐 Frama-C （免责声明：我在 Frama-C 上工作，但不在与 ACSL 规范有关的部分）。对于 C 程序的测试生成，我听说过关于 CUTE 的好消息。
I am not familiar with CML, but the article you link starts with the statement that it is for specification of non-functional requirements.
JML is for functional requirements of Java programs (okay, the line is blurry, but I think the CML article is using the word in the same sense as this sentence). An equivalent of JML for C programs (therefore also purely for functional requirements) is ACSL.
For formal verification, I can only recommend Frama-C (disclaimer: I work on Frama-C but not on a part that has to do with ACSL specifications). For test generation for C programs, I have heard good things about CUTE.
“针对”C 的正式规范？
我知道需要正式指定的工作 C: C 的指称语义。
如果您想指定 C 程序的功能，则可以使用属性规范语言 可能是一个有用的起点。
Formal specification "for" C?
I know of work to formally specify C: Denotational Semantics for C.
If you want to specify what C programs do, then the Property Specification Language might be a useful place to start.
C 语言的验证系统至少有 4 个：
中提供） frama-c。您还需要安装why才能使 jessie 工作）(1) 适用于用 MISRA-C 或类似语言编写的安全关键型嵌入式 C 程序。
(2) 适用于使用 Microsoft C 编译器构建的多线程系统。
我对（3）和（4）知之甚少。
There are at least 4 verification systems for C around:
frama-c. You'll need to installwhytoo to make jessie work)(1) is intended for safety-critical embedded C programs written in MISRA-C or similar.
(2) is intended for multithreaded systems built using the Microsoft C compilers.
I know rather less abiout (3) and (4).