frama-c - C/frama-c 和 Spark-ada 之间的等价性

Question

我正在研究框架 Frama-c，我想知道 C/Frama-c 和 Spark Ada 之间是否存在等价关系。我知道比较这些不同的语言似乎很奇怪，但是在阅读了David A. Wheeler 的文章、Johannes Kanig 的比较和一些 SPARK 的用户手册之后，我很难猜测 SPARK 和 C/Frama-c/ACSL 是否给出相同的证明稳健性和相同的代码可靠性。

非常感谢您提前提供您的观点/经验！

PS：我对frama-c很陌生，对SPARK编程知之甚少。

Answer 1

我不知道 Frama-C，但 SPARK 证明是——据我所知——它们是绝对的保证。使用 SPARK，您可以在一定程度上选择您想要证明的数量。

基本级别是证明不存在运行时错误（异常），但 SPARK 将尝试证明您插入到源文本中的所有断言（包括前置条件和后置条件）。因此，如果您插入记录一些功能需求的断言，那么保证（假设您的 SPARK 工具可以证明断言正确）扩展到这些功能需求。