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

Dear Aaron,

I can confirm that neither alt-ergo nor the other automatic provers prove your example from the tutorial.
(I am running Beryllium on Mac OS X.)

However, I can show you the specification of a function similar to max_seq.c
The main difference is that our function max_element does not directly return the maximum value
in the array but rather the index of the maximum element.
(This allows, by the way, that max_element works for n == 0 as well.)

You will also notice that our specification is slightly longer than that of max_seq.c
This is partially due to the fact that we specify not only that our functions returns one maximum value
but the _first_ maximum value in the array.

In our example, both alt-ergo, z3, yices, cvc3, and simplify can proof the correctness of max_element.
I think you can easily adopt our specification to the one needed for max_seq.


Regards Jens



Am 11.11.2009 um 06:02 schrieb Aaron Rocha:

> 
> /*@ 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


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091111/2e16db35/attachment.htm 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: max_element.c
Type: application/octet-stream
Size: 723 bytes
Desc: not available
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091111/2e16db35/attachment.obj 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20091111/2e16db35/attachment-0001.htm