Consider the following algorithm, where A[1..n] is an array of integers with n \ge 1.

1  function ALG(A[1..n])
2      s = 0
3      for k = 1 to n do
4          # INVARIANT HOLDS HERE
5          if A[k] % 2 = 0 then
6              s = s + A[k]
7      return s

Prove that the following invariant holds every time execution reaches the line marked # INVARIANT HOLDS HERE — that is, at the start of the loop body, for each value of k the loop runs with:

s is the sum of the even elements of A[1..k-1]  (when k = 1, A[1..0] is empty, and an empty sum is 0)

A complete answer contains two parts, and both are marked:

• Initialisation (2 marks) — the invariant is true the first time the marked line is reached, when k = 1.
• Maintenance (4 marks) — assuming the invariant is true at the marked line for one value of k, show it then holds for k + 1 — and so is true at the next visit to the marked line, if the loop runs again. Consider what one pass of the loop body does in every case that can occur.

You do not need to prove the termination step, and you do not need to prove that the loop stops.

Type your answer as plain text: write ranges like A[1..k-1], and use ordinary words freely — full mathematical notation is not required. You may draft on the paper provided, but only what you type into Moodle is marked.