Making very useful progress with the indexof example.  I think that's about as far as I can take it now, since it doesn't even verify in Whiley and I haven't decided what the loops invariants need to be.