int[] fib(int n) //@requires n >= 0; //@ensures \length(\result) == n; { int[] F = alloc_array(int, n); F[0] = 0; F[1] = 1; for (int i = 0; i+2 < n; i++) //@loop_invariant i >= 0; { F[i+2] = F[i+1] + F[i]; } return F; }