Proof of linear search?
What about using a "goal" variable initialized to NIL and taking as invariant "After iteration i, the goal variable contains an index $0 \leq j &lt; i$ such that $A[j] = v$ if there exists one (in the range $\{0, \cdots, i - 1\}$), or NIL otherwise" ?