Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification of axiomatization

  • Subject: [Frama-c-discuss] Verification of axiomatization
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Tue, 7 Apr 2009 00:58:48 +0200
  • References: <49DA2031.5030905@insa-lyon.fr>
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.

Pascal