This is a followup to yesterday's session, especially for those who could not attend the 2nd half. We finished correcting most of the homework and we devoted part of the session to model the exercises in Rodin.

We had time to do the "Odd way" to calculate n^2 only, as we bumped into some technical hurdles. I believe that the mail Ignacio sent sheds light on how to solve the problem. Please howl if that is not the case.

For those who attended the full lecture: please model on your own the Russian multiplication in Rodin, including correctness and termination (as we did in th "Odd n^2". Note: Rodin has 'mod' among the arithmetic operators. Some invariant may not be proven straight away. Nothing to worry about, and this it can be different for each of you. There are reasons for that - more on it in the next session and the cure is easy.

For those who did not do that last part: *please* make sure to install Rodin as per the instructions in the last set of slides, import the IntegerDivision example to see what a model and the editor looks like, and try to model the n^2 and the Russian multiplication calculations. In the next session I plan to show something with the Russian multiplication example and I would like you to be up-to-date with it. And in coming sessions ad homeworks I plan you to use Rodin extensively.

Rodin can be initially disconcerting, but it is only 10 minutes until one understands how the editor works. I suggest that your pair up with some of your classmates for a quick primer. Ask in the mailing list if you experience problems.

Best,