In more detail (pay careful attention to < vs. <)
(("k < i) a[k] != v ô i < a.length) before the iteration
(("k < i) a[k] != v ô i < a.length) after the body
a[i] != v ô i < a.length the iteration reveals
But then i = i +1;
(("k < i) a[k] != v ô i < a.length) starting the next iteration