@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 = 1;

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

  while (i < n) {
     a[i] = a[i] * 2;
     i = i + 1;
  }

@end
--

     all(k, 0:i-2, a[k] = 2*k) &&

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