我记得不久前读过一些关于 C 的正式规范语言的内容,但现在我需要它却找不到它。
它受到 JML 的启发,就我所见使用相同的语法。
我发现它的唯一参考是一篇论文,但我所说的比这更精致。
如果这给你敲响了警钟……
如果没有人知道这一点,我会很高兴听到一种在 C 中进行形式验证和自动测试生成的方法。
提前致谢。
我记得不久前读过一些关于 C 的正式规范语言的内容,但现在我需要它却找不到它。
它受到 JML 的启发,就我所见使用相同的语法。
我发现它的唯一参考是一篇论文,但我所说的比这更精致。
如果这给你敲响了警钟……
如果没有人知道这一点,我会很高兴听到一种在 C 中进行形式验证和自动测试生成的方法。
提前致谢。
C 周围至少有 4 个验证系统:
frama-c
。您why
也需要安装才能使 jessie 工作)(1) 适用于以 MISRA-C 或类似语言编写的安全关键型嵌入式 C 程序。(2) 适用于使用 Microsoft C 编译器构建的多线程系统。我对 (3) 和 (4) 知之甚少。