1. Unfortunately there seem to be some mistakes in past exam papers/their solutions. Below is a list of some errors, thanks very much to Alistair O'Brien and Ben Andrew for reporting them. Note: I have not checked in detail all the definitions from the lectures of those previous years, and so I don't want to exclude the possibility that what looks like errors now is due to a subtly different logical setup back then. 2. Separately from that, there are two errors in the Exercises for Hoare Logic sheet, thanks very much to Mihailo Milosevic for reporting these. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1. Exam questions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2019 Paper 8) Question 7) Please ignore the solutions to d) and e) which, at least given the separation logic definitions we used this year (22/23), look like they are incorrect: using separating conjunction in combination with pure assertions in a way that allows for unintended memory leaks. However, I have not worked through the proof in detail to really confirm. 2020 Paper 8) Question 8) a) i) A disjointness condition on program variables seems to be missing here to make the argument: mod(C1) ∩ fv(P2) = ∅ ∧ mod(C2) ∩ fv(Q1) = ∅ e) The program needs to be fixed, it is missing an update of M: if N < M then X := Y; M := N else skip​ 2021 Paper 8) Question 8) a) There are a couple of things here: - The pre-condition should have "... ∧ 1 ≤ S" instead of "... * 1 ≤ S". - The assignment "B := B + 2^S" in the "then" part of the if-then-else should be "B := R + 2^S". - And then finally: The exam question's post-condition has the wrong shape. It has the shape "... * (... R = align(...))", where the separating conjunction will not behave as intended with respect to the (pure) alignedness assertion. Instead, we should have the following assertion (or something equivalent) as the post-condition of the exam question (not its solution): (R = 0 => block(B,E−B)) ∧ (R ≠ 0 => ((block(B,E−B) * block(R,2^S)) ∧ R = align(R,2^S))) b) C_alloc is not precisely defined, which likely adds confusion. C_alloc should probably be the program from (a). e) And then something is wrong here, too. Probably best to just ignore this one. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2. Exercise sheet %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Exercise 45: something’s wrong here. A counterexample is, for instance, alpha = [1], beta = []. I suspect it might just be the specification that’s wrong here, but I haven’t worked through the proof yet for a corrected specification. Exercise 46: the code is broken, it does not always terminate. Please ignore both exercises.