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