--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on November 2009 ---
[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