--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on November 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C vs Ada/SPARK



Hi everybody, 

I am not very familiar with either Frama-C or Ada/SPARK. I am wondering whether anyone in the list would be able to comment on how they compare against each other. It seems as though Frama-C has a stronger focus on mathematic proofs whereas SPARK is more like an static analyzer. Although I have never written any Ada code, I reckon the task of proving the correctness of Ada code is easier than C code - particularly in the case of SPARK since only a subset of Ada is allowed. 

Has anyone used/compared both? Can you comment on it?

Thanks,
Iran Rocha


      __________________________________________________________________
Ask a question on any topic and get answers from real people. Go to Yahoo! Answers and share what you know at http://ca.answers.yahoo.com