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