@requires n >= 1 

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

@program 

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

  i = 0;

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

     (a[i-1] < 0 ==> b[i-1] = 0) &&
     (a[i-1] >= 0 ==> b[i-1] = a[i-1]) &&

     i >= 0 && i =< n

  while (i < n) {
     if (a[i] < 0) 
        b[i] = 0;
     else 
        b[i] = a[i];
     i = i + 1;
  }

@end
--

     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