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

[Frama-c-discuss] Newbie question



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                    |