PRE$-$condition: a $!=$ null,

a$.$length $>0,$ and

a$[$a$.$length$-1]==$ x

$1.$ int opt$\_$search$($int$[]$ a$,$ int x$)\{$

$2.$

int i;

$3.$

$4.$

$5.$

$6.$

$7.$

$8.$

$9.$

$10.\}$

for $($i $=0$; a$[$i$]!=$ x; i$++)\{$

$//$ Empty body

$\}$

if $($i $<$ a$.$length$-1)\{$

return i;

$\}$

return$-1$;

POST$-$condition: If there exists i such that i $>=0,$ i $<$ a$.$length$-1$

and a$[$i$]==$ x$,$ then return i$,$ otherwise return$-1.$

Assume a has length N $+1$ such that $\{$ a$[0],$ a$[1],...,$ a$[$a$.$length$-2]\}$ is a set of

N distinct elements, which may or may not contain the target element x$,$ but

a$[$a$.$length$-1]==$ x $1.$Give the best loop invariant to prove that opt search returns with the

POST$-$condition satisfied. $2.$Verify the initialization condition of the loop invariant from part $($a$).3.$Verify the maintenance condition of the loop invariant from part $($a$).$