@requires n >= 1 && 
          all(k, 0:n-1,  a[k] = k)

@ensures all(k, 0:(n-1), a[k] = 2*k)

@program 

  @var i, n : int
  @var a : int[]

  i = 0;

  @invariant 
     all(k, 0:i-2, a[k] = 2*k) &&
     (i > 0 ==> a[i-1] = 2*(i-1)) && 
     all(k, i:n-1, a[k] = k) &&
     i =< n
  while (i < n) {
     a[i] = a[i] * 2;
     i = i + 1;
  }

@end
--