The timing and testing code for this lecture (find-test.c0 and
find-time.c0) lives in the directory for the next lecture
(06-binsearch). Both lectures involve a file "find.c0" implementing
the same specification:

int search(int x, int[] A, int n)
//@requires 0 <= n && n <= \length(A);
//@requires is_sorted(A, 0, n);
/*@ensures (-1 == \result && !is_in(x, A, 0, n))
        || ((0 <= \result && \result < n) && A[\result] == x);
  @*/
  ;

The safety of all the array accesses in search() is described in
points-to-reasoning in the file find-safe.c0, and the correctness of
assertions is described in find-correct.c0 and in more detail in
find-correct-detailed.c0. This is not a perfect way to think about the
problem, but at least for this problem it's worth first reasoning
about why every array access is safe and then reasoning about
correctness taking for granted that all the accesses are safe.