CODEWITHSUNDEEP
frama-cspark-adaspark-2014
Eliott.CH
Eliott.CH

Reputation: 25

Equivalence between C/frama-c and Spark-ada

I'm studying the framework Frama-c, and I'm wondering if there is an equivalence between C/Frama-c and Spark Ada. I know that it can seem quite odd to compare such different languages, but after reading David A. Wheeler's article, Johannes Kanig's comparison and a bit of SPARK's user manual, I am struggling to guess if SPARK and C/Frama-c/ACSL give the same proof robustness and the same code reliability.

Thank you a lot in advance for giving your point of view / experience !

PS: I'm quite new to frama-c and I don't know much about SPARK programming.

Upvotes: 0

Views: 319

Answers (1)

Jacob Sparre Andersen
Jacob Sparre Andersen

Reputation: 6601

I don't know Frama-C, but SPARK proofs are - as I understand - them absolute guarantees. With SPARK you can to some extend select how much you want proofs of.

The basic level is to prove absence of run-time errors (exceptions), but SPARK will attempt to prove all assertions (including pre- and post-conditions) you insert into your source text. So if you insert assertions, which document some functional requirements, then the guarantees (assuming that your SPARK tools can prove the assertions correct) extend to those functional requirements.

Upvotes: 0

Related Questions