Following up on the class discussion of insertion sort,
please write **C code decorated with assertions** for a binary-search
function with this prototype:

```
int *binsearch(int needle, int *haystack, int n);
```

where

`haystack`

is a*sorted*array of length`n`

.- If the value
`needle`

appears anywhere in`haystack`

,`binsearch`

returns a pointer to a location in`haystack`

containing`needle`

. - If the value
`needle`

appears nowhere in`haystack`

,`binsearch`

returns`NULL`

. - In either case, the contents of
`haystack`

are unchanged.

Please write precondition, postcondition, loop invariants, and any intermediate assertions you need to get working. The **loop invariant can be hard to get right**; you'll want to pay close attention.

The running time of your function should be *O(log n)*.

**In time for class on Wednesday, March 10**, please

- Come up with at least one useful abbreviation in addition to
`SORTED[x..y)`

- Give the definition of the abbreviation
- Give one or more proof rules for the abbreviation
- Use the abbreviation to write down what you think should be the invariant
- Decorate your code with assertions
- Come to class with either
- a proof that your decorated code is correct
- an indication of where you got stuck

- Come to class with an argument about
*why your function terminates*

Back to list of assignments