T Naughton, CS NUIM, Back to SE120 home

Remove everything from your desk except pens/pencils. Paper will be provided. Answer all questions. Remember to be mathematically precise in all of your answers. You have until 15:50. You can leave whenever you are finished.

Q1 What is the meaning of the Hoare triple {P}S{R} if it evaluates to true? [2 marks]

Q2 Prove that the following program is correct. [5 marks]

{true}
if odd(x) then
   y := x + 2
else
   y := x + 1
fi
{odd(y) ^ y > x}

Q3 Calculate the loop invariant P for the following program. [3 marks]

{x > 0 ^ z >= x}
y := 0;
{P}
while (x + y) < z do
   y := y + 1
od
{x + y = z}