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] Newbie question

  • Subject: [Frama-c-discuss] Newbie question
  • From: hxdg21 at yahoo.com (Aaron Rocha)
  • Date: Tue, 10 Nov 2009 21:02:24 -0800 (PST)
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.