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

[Frama-c-discuss] Newbie question



Hi,

If you want to learn the Jessie plugin, please use the jessie tutorial 
instead :

  http://frama-c.cea.fr/jessie_tutorial_index.html

The example max_seq given in ACSL tutorial is not annotated properly to 
be proved.

About provers to install on Linux: see the prover tips page of the Why tool.

- Claude


Aaron Rocha wrote:
> 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.
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |