Lab 1, 12/11, Hoare Logic Solutions to selected exercises Proposed plan: :00-:10 (10m): Discuss plan for session and revise material :10-:25 (15m): Group discussion and solution to Exercise 1 (derivation tree + decorated program) :25-:55 (30m): Solve Exercises 2, 3, and 4 in breakout rooms (2/3 students) :55-:10 (15m): Group discussion and solution of Exercises 4 and 5 :10-:25 (15m): Solve Exercise 6 in breakout rooms (2/3 students) :25-:30 (5m): Conclusion
Lab 2, 19/11, Introduction to Dafny Solutions to selected exercises Proposed plan: :00-:10 (10m): Discuss plan for session and revise material :10-:25 (15m): Group discussion and solution to Exercise 1.1 (integer division) :25-:55 (30m): Solve Exercises 1.2, 1.3, and 1.4 in breakout rooms (2/3 students) :55-:10 (15m): Group discussion and solution of Exercises 1.3 and 3 :10-:25 (15m): Solve Exercises 4, 5, and 6 in breakout rooms (2/3 students) :25-:30 (5m): Conclusion
Lab 3, 26/11, Reasoning about Functions in Dafny Solutions to selected exercises Original file: Lab3_exercises.dfy Proposed plan: :00-:10 (10m): Discuss plan for session and revise material :10-:25 (15m): Group discussion and solution to Exercises 1 and 2 :25-:10 (45m): Solve Exercises 3, 4, 5 and 6 in breakout rooms (2/3 students) :10-:25 (15m): Group discussion and solution of selected exercises :25-:30 (5m): Conclusion
Lab 4, 02/12, Dynamic Frames in Dafny Solutions to selected exercises: Exercise 2 and Exercise 3 Proposed plan: :00-:10 (10m): Discuss plan for session and revise material :10-:25 (15m): Group discussion and solution to Exercise 1 :25-:10 (45m): Solve Exercises 2 and 3 in breakout rooms (2/3 students) :10-:25 (15m): Group discussion and solution of selected exercises :25-:30 (5m): Conclusion
Lab 5, 10/12, Separation Logic Solutions Proposed plan: :00-:10 (10m): Discuss plan for session and revise material :10-:25 (15m): Group discussion and solution to Exercises 1.1, 1.2, and 2.1 :25-:10 (45m): Solve Exercises 1, 2, and 3 in breakout rooms (2/3 students) :10-:25 (15m): Group discussion and solution of selected exercises :25-:30 (5m): Conclusion
Lab 6, 17/12, Project development The plan of this lab session is to work on the second project.
Exercise in the book "Software Abstractions: Logic, Language, and
Analysis" by D.J.
A.3.6 (Surgeon's Gloves). In
order to solve this task, one need to model the fact that the surgeon
can wear multiple gloves at the same time. Sequences (seq) can be used for
that. One also needs to model
all different operations. One of those operations is 'turning a glove inside
out'.
