int product(int a, int n) {
  // Fonction product(a, n) returns a*n if n is greater or equal to 0
  //@ requires n >= 0;
  //@ ensures result == a * n ;
  int r = 0;
  //@ label start ;
  while (n != 0) {
    // We give a loop invariant (for the correction) and a variant (for termination)
    //@ invariant r + a*n == at (a, start) * at (n, start) && n >= 0 ;
    //@ variant n;
    if (n%2 != 0) {
      n--;
      r += a;
    }
    //@ assert n % 2 == 0 ;
    n /= 2;
    a *= 2;
  }
  return r;
}