(a) Given an appropiate loop invariant
(b) Use your loop invariant from (a) to prove partial correctness (when loop terminates)
(c) Define an appropriate expression for the purpose of proving termination.
Solution:
a)
(1) $0 \leq i \leq j$
(2) not sure
(b)
Suppose the loop terminates
By $LI(1)$ $i \leq j$
By loop exit condition $i \geq j$
hence $i = j$ (*)
Not sure how to solve rest
(c)
$e = j - i + 1$ (pretty sure this is right)
How do I do this?