--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2009 ---
For information, here is the max_seq example with sufficient annotations to prove the code. Notice: - the use of \at(p,Pre) in the loop invariant, needed because p is modified by the loop (the previous invariants were *wrong*) - the premisse 0 <= j < i instead of 0 <= j <= i in the quantified loop invariant Hope this helps, - Claude /*@ requires n > 0; requires \valid(p+ (0..n-1)); assigns \nothing; ensures \forall integer i; 0 <= i <= n-1 ==> \result >= p[i]; ensures \exists integer 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 0 <= i <= n; @ loop invariant 0 <= e <= n-1; @ loop invariant p == \at(p,Pre)+i; @ loop invariant \forall integer j; 0 <= j < i ==> res >= *(\at(p,Pre)+j); @ loop invariant \valid(\at(p,Pre)+e) && \at(p,Pre)[e] == res; @ loop variant n-i; @*/ for(i = 0; i < n; i++) { if (res < *p) { res = *p; //@ ghost e = i; } p++; } return res; } -- 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 |