Exercise 2 is about program verification with Boogie. If possible, please download and install Boogie before coming to the session: http://research.microsoft.com/en-us/projects/boogie/