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

[Frama-c-discuss] Verification of axiomatization




CUOQ Pascal wrote:
> Hi Nicolas,
> 
>> Is there a method to verify an axiomatization in an annotated C file ?
> 
> You know, what with automatic theorem provers that are
> barely able to prove a couple of simple properties as things stand
> on the one hand, and G?del's second incompleteness theorem on
> the other hand, I think there is potential for some really good
> sarcastic remarks here.
> I really wish I knew more about these things.
> I'd be cracking jokes... you couldn't stop me.
> 
> More seriously, this reminds me of an interesting discussion
> at the training session (well, the beginning of a discussion.
> The only bad thing about that day was that it was too short).
> If we are going to use first-order logic as an alternative
> programming language in which alternative versions of the
> C functions are defined and composed... but I am getting
> ahead of myself. For those who weren't
> there, I should provide context by saying that Virgile took
> advantage of his talk to match a sort function and its
> specification in real time...
> Now, if we are going to use first-order logic as 
> an alternative programming language, 
> we will at some point have to make it acceptable
> as a programming language.
> So the future probably holds a lot of module systems,
> syntactic restrictions, static consistency checks,...
> But to answer your question, and to the best of my knowledge,
> we don't have much of all that for now.

I don't understand why you are so pessimistic, Pascal.
The answer is simple: just realize your axiomatization in Cuoq. Sorry: I 
meant in Coq.

- Claude