Part 2 (Week 08 -- Week 14)
- Lab 1, 14/11, Hoare Logic
- Lab 2, 21/11, Introduction to Dafny
- Lab 3, 28/11, Reasoning about Functions
- Lab 4, 05/12, Dynamic Frames in Dafny
- Solution to exercise 2
- Exercise 1 is almost identical to StackOdd (see Lecture 10)
- Lab 5, 12/12, Lab used to work on the project
- Lab 6, 19/12, Assertions in Separation Logic
Part 1 (Week 01 -- Week 07)
Exercises for labs week 21 -- 25 Oct
Solve the exercise A.3.6 (Surgeon's Gloves) from the reference book.
In
order to solve this task, one need to model the fact that the surgeon
can wear multiple gloves at the same time. Sequences can be used for
that, 'seq A' is a sequence of elements of A. One also needs to model
all different events. One of those events is 'turning a glove inside
out'.
(Partial solution below.)
Exercises for labs week 14 -- 18 Oct
Solve the exercises
- A.2.1 (Telephone Switch)
- A.2.3 (Inmate Assignment)
(Solution suggestions below.)
Exercises for labs week 7 -- 11 Oct
Solve the following exercises proposed in http://alloytools.org/tutorials/day-course/
Exercises for labs week 30 Sept -- 4 Oct
The Alloy tutorial available at http://alloytools.org/tutorials/online/
Exercises for labs week 23 -- 27 Sept
There is an exercise sheet W1-FOL in "Lab exercises". The recommended exercises are
Section 1.2: 1, 2.
Section 1.3: 1, 3.
Section 2: 1-13.