COMP2111 Assignment 3 2020 Term 1
Due: Monday, 27th April, 12:00 noon
Submission is through give and should be a single pdf file, maximum size 4Mb. Prose should be typed, not
handwritten. Use of LATEX is encouraged, but not required. See the course website for detailed submission
instructions.
Discussion of assignment material with others is permitted, but the work submitted must be your own in
line with the University’s plagiarism policy.
Problem 1 (30 marks)
Consider this program P written in the language L. Assume all variables and constants represent natural
numbers (including zero)1.
n := N;
r := 1;
while n 6= 0 do
r := X × r;
n := (n – 1);
od
(a) The above program should satisfy the postcondition r = XN given the precondition True. Prove this
using Hoare Logic. You will need to:
| (i) Determine an appropriate loop invariant for the while loop. (ii) Write a proof outline for the program with assertions after every statement. (iii) Show that your invariant implies the postcondition when the loop guard is false. (iv) Show that your invariant is preserved by the loop body. (v) Show that your invariant is established by the code above the loop. Be sure to prove any implications arising from use of the rule of consequence. |
(5 marks) (8 marks) (3 marks) (2 marks) (2 marks) |
| (b) Show termination of the above algorithm. Remember that all variables represent natural numbers. | |
| You will need to: (i) Determine an appropriate loop variant for the while loop. (ii) Add assertions to demonstrate progress for the loop variant. (iii) Show positivity for the loop variant. Be sure to prove any nontrivial implications required to discharge the proof. |
(3 marks) (5 marks) (2 marks) |
1We define 00 = 1 and 0n = 0 for all n > 0
1
Problem 2 (50 marks)
Here is a more efficient algorithm, Q, to compute the same result as P. We use ÷ to denote integer division,
which always rounds down, i.e. n ÷ m = bmn c. Note that therefore (n ÷ m) × m = n only when m j n.
x := X;
n := N;
r := 1;
while n ≥ 1 do
if 2 j n then
x := x × x
n := n ÷ 2
else
r := x × r;
x := x × x;
n := (n – 1) ÷ 2;
fi
od
(a) Once again the above program should satisfy the postcondition r = XN given the precondition True.
Prove this using Hoare Logic, similarly to the previous question. That is, you will need to:
| (i) Determine an appropriate loop invariant for the while loop. (ii) Write a proof outline for the program with assertions after every statement. (iii) Show that your invariant implies the postcondition when the loop guard is false. (iv) Show that your invariant is preserved by the loop body. (v) Show that your invariant is established by the code above the loop. Be sure to prove any implications arising from use of the rule of consequence. |
(8 marks) (12 marks) (4 marks) (3 marks) (3 marks) |
| (b) Show termination of our improved algorithm. You may need to slightly adjust your verification in | |
| other places to show this. Once more you will need to: (i) Determine an appropriate loop variant for the while loop. (ii) Add assertions to demonstrate progress for the loop variant. (iii) Show positivity for the loop variant. Be sure to prove any nontrivial implications required to discharge the proof. |
(5 marks) (10 marks) (5 marks) |
2
Problem 3 (20+ marks)
Recall from Week 3 that we can compute fibonacci numbers by exponentiating a matrix:
1 1 1 0N =
| fibfib (n(+n)1) | fibfib (n(-n)1) |
(a) How can we use this fact to transform our fast algorithm Q above to compute the nth fibonacci
number in log time? Write a new version of Q that is structurally similar, but instead computes the
nth fibonacci number. Assume matrix multiplication and matrix variables are added as primitives to
| L. Think about how you can generalise numeric operations to matrix ones. | (20 marks) |
| (b) Bonus: Prove that your new version of Q does indeed compute the Nth fibonacci number with Hoare | |
| logic. | (10 marks) |
3
The post COMP2111 Assignment appeared first on My Assignment Online.
