Hi. I have received several questions regarding section 3.3 of HW2. Some of you have reasoned along the lines of "when the event Finish is enabled, then f(r) = y and we have found what we wanted". That is true, but it is not an answer. First of all, Finish might never be enabled; we never proved explicitly it was going to be enabled. Second, and more important: Finish is an artifact that appears in the model only to highlight a condition in which a sequential algorithm would have exited from a loop. But it does not do anything, and we may as well remove it and nothing changes in the model: all the proofs we discharged can still be discharged. So, let us assume that Finish does not exist and things will be clearer.
Section 3.3 asks: how would you prove that IF the model eventually stops, then we will have found the location of 'v'? And I am asking you to find out a logic formula such that if it can be inferred from the axioms and the invariants, then the model eventually finds the location of 'v'. And, furthermore, you should be able to introduce this formula in Rodin as an invariant (perhaps marked as 'theorem') and, if Rodin discharges the formula, then you would have proved that the model eventually finds an r s.t. f(r) = v.
Since this clarification is coming somewhat late, I will be accepting homework until Monday, April 4th, 23:59 without any penalty.
Greetings,