Q$1[14]$ Suppose a and $b$ are constant integer arrays with domain

$\{0,..,n\}$ where $n1$ with a increasing $)$

and $b$ decreasing $).$ You may assume

that $a(0)b(0)$ and $a(n)>b(n).$ We need to find where the arrays cross.

In particular we want to find the largest value for $p$ where $a(p)b(p)$

$f=($:$a(p^{\text{'}})b(p^{\text{'}}{)}^{{?}^{?}}a(p^{\text{'}}+1)>b(p^{\text{'}}+1)$:$)$

Use the method of binary search.

$($a$)[6]$ Give a loop invariant I.

I is

$($b$)[2]$ Let $g=(($:I:$)=>f)$ and $m=($:$a^{\text{'}}=a^{{?}^{?}}{b}^{\text{'}}=b^{{?}^{?}}{I}^{\text{'}}$:$)$ Give an initializa$-$

tion command that refines $m.$

$m$

$($c$)[2]$ Give a guard expression A such that $($:notA:$)=>g$ skip

$A$ is

$($d$)[2]$ Give a loop body command that refines $h=($:$A^{{?}^{?}}I=>I^{\text{'}}{?}^{{?}^{?}}{a}^{\text{'}}=a^{{?}^{?}}{b}^{\text{'}}=b$:$)$

and decreases a bound expression.

$h$

$($e$)[2]$ Give a bound expression with which your loop can be shown to

terminate.