--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on November 2009 ---
Hi everybody, I am new to Frama-C and to the world of assisted mathematical proofs. Basically, I am a C developer who is interesting in writing code that can be verified. I ran across Frama-C and it looks like just the type of thing I was looking for. I am having a little bit of a hard time getting started though. I am on Linux and it looks like only a selected number of proof assistants are available on this platform. It sounds to me as though Coq would be the best one. The problem is that, if I use Coq, I have to actually fill the proof in (after make -f <source file>.makefile coq) and I am not familiar with Coq yet. So I am using Alt-Ergo instead. But Alt-Ergo fails to prove the preservation of loop invariants in this code from the tutorial: /*@ requires n > 0; requires \valid(p+ (0..n-1)); assigns \nothing; ensures \forall int i; 0 <= i <= n-1 ==> \result >= p[i]; ensures \exists int e; 0 <= e <= n-1 && \result == p[e]; */ int max_seq(int* p, int n) { int res = *p; int i = 0; //@ ghost int e = 0; /*@ loop invariant \forall integer j; 0 <= j <= i ==> res >= *(p+j); loop invariant \valid(p+e) && p[e] == res; */ for(i = 0; i < n; i++) { if (res < *p) { res = *p; //@ ghost e = i; } p++; } return res; } Do you run frama-c on Linux? If so, what proof assistants are you using? If Coq is the way to go, is there some sort of gentle introduction on how to use Coq with Frama-c? Thanks in advance __________________________________________________________________ Yahoo! Canada Toolbar: Search from anywhere on the web, and bookmark your favourite sites. Download it now http://ca.toolbar.yahoo.com.