Suppose a and b are constant integer arrays with domain {0, .., n} where n ≥ 1 with a increasing (∀i, j ∈ {0, .., n} · i ≤ j ⇒ a(i) ≤ a(j)) and b decreasing (∀i, j ∈ {0, .., n} · i ≤ j ⇒ b(i) ≥ b(j)). 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′) ≤ b(p′) ∧ a(p′ + 1) > b(p′ + 1)⟩
Use the method of binary search.
1. Give a loop invariant I.
2. Let g = (⟨I⟩ ⇒ f) and m = ⟨a′ = a ∧ b′ = b ∧ I′⟩ Give an initialization command that refines m.
3. Give a guard expression A such that ⟨¬A⟩ ⇒ g ⊑ skip.
4. Give a loop body command that refines h = ⟨A ∧ I ⇒ I′ ∧ a′ = a ∧ b′ = b⟩ and decreases a bound expression.
5. Give a bound expression with which your loop can be shown to terminate.

(a) q, b, and a are constant functions. Let g = ⟨x′ = q(x, a(y))⟩ and f = ⟨x′ = q(b(x), a(y + 1))⟩. Give an assignment command h such that f ⊑ h; g
(b) Use the forward substitution law for assignment to show that
f ⊑ h; g.


For integers X and Y design an efficient (log Y time) iterative algorithm to compute X^Y.
Complete the following proof outline {x = X ∧ y = Y ≥ 0} ? {z = X^Y}
You should assume that variables x, y, and z hold mathematical integers —thus there is no overflow– and that the operations assignment, +, -, ×, ÷, ‘odd’, and ‘even’ each take 1 unit of time, as do any comparisons. Be sure to state the invariant of your loop. Note that the solution to this problem is useful in the efficient
implementation of the RSA algorithm, which is used widely for encryption.

Consider the following specification where a and b are arrays of integers of length n
f = ⟨∀i ∈ {0, ..n} · b′(i) = (∑ j ∈ {0, .., i} · (−1)^j × a(j))⟩
E.g. a = [7, 2, 6, 8], b′ = [7, 5, 11, 3].
Read the whole question before beginning to answer. The idea is to
develop a command of the form
f ⊑ m0; while A do h0
The command should run in Θ(n) time.
(a) Propose a loop invariant I
Let g = (⟨I⟩ ⇒ f). Let m = ⟨I′ ∧ a′ = a⟩ so that f is refined by m; g.
(b) Give a command that refines m.
(c) Give an expression A and such that
I ∧ ¬A ⇒ ∀i ∈ {0, ..n} · b(i) = (∑ j ∈ {0, ..i} · (−1)^j × a(j))
is true for all states, i.e., so that ⟨¬A⟩ ⇒ g is refined by skip.
(d) Propose a bound expression for the loop.
Let h = ⟨A ∧ I ⇒ I′ ∧ a′ = a⟩ so that
g is refined by (if A then (h; g) else skip)
(e) Give a command that refines h and that makes the bound
expression smaller.