C/frama-c与Spark-ada的等价性

Question

我正在研究Frama-c框架，我想知道C/Frama-c和Spark Ada之间是否有等价物。我知道比较这种不同的语言看起来很奇怪，但在阅读了David A. Wheeler's article、Johannes Kanig's comparison和一些SPARK的用户手册后，我很难猜测SPARK和C/Frama-c/ACSL是否提供了相同的证明健壮性和相同的代码可靠性。

提前感谢您给出您的观点/经验！

PS:我是frama-c的新手，我对SPARK编程了解不多。

Answer 1

我不知道Frama-C，但据我所知，火花证明是绝对的保证。有了SPARK，你可以在某种程度上选择你想要的证据。

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