私はフレームワーク Frama-c を研究していますが、C/Frama-c と Spark Ada の間に同等性があるかどうか疑問に思っています。このような異なる言語を比較するのは非常に奇妙に思えるかもしれませんが、David A. Wheeler の記事、Johannes Kanig の比較、および SPARK のユーザーマニュアルを少し読んだ後、SPARK と C/Frama-c/ACSL が与えるかどうかを推測するのに苦労しています。同じ証明の堅牢性と同じコードの信頼性。
あなたの視点/経験を与えてくれてありがとう！
PS: 私は frama-c を初めて使用し、SPARK プログラミングについてあまり知りません。