C语言的Java建模语言?
问题描述:
我记得在前一段时间阅读了有关C的正式规范语言的一些内容,但现在我找不到它,我需要它。C语言的Java建模语言?
它的灵感来自于JML,只要我看到相同的语法。
我发现的唯一参考是一个paper,但是我所说的比这更好。
如果这听起来很耳熟你...
如果没有人知道这一点,我会很高兴听到办法做正式验证和自动测试代C.
谢谢提前。
答
Formal specification for“C?
我知道工作正式指定 C:Denotational Semantics for C。
如果你想指定什么 C程序做,那么Property Specification Language可能是一个有用的开始。
答
有对C围绕至少4个验证系统:
- 埃舍尔Ç验证。 [我与此连接。]
- Microsoft VCC。
-
Frama-C与杰西插件(在Debian/Ubuntu的可在包
frama-c
。您需要安装why
太让杰西工作) - VeriFast。
(1)适用于使用MISRA-C或类似软件编写的安全至关重要的嵌入式C程序。 (2)适用于使用Microsoft C编译器构建的多线程系统。 我知道比较少(3)和(4)。