1) Reformulate the three pre-post specifications from the lecture 22.9 to capture divison on the real numbers instead of the natural numbers.

2) Assume the variables dividend, divisor, quotient and rest are of type real. How should the three pre-post specifications from the lecture be reformulated to still specify integer division?

3) To what extent do the pre-post specifications from Exercise 2 refine the pre-post specifications from Exercise 1 (do they strengthen the assumption or weaken the guarantee)?  

4) To what extent do the pre-post specifications from Exercise 1 refine the pre-post specifications from Exercise 2 (do they strengthen the assumption or weaken the guarantee)?

5) Assume we work with binary numbers consisting of exactly 8 bits. Write pre-post specifications for addition, subtraction and multiplication.

6) Reduce the set of possible traces for the sequence diagram on Foil 27 by adding one message (arrow decorated with message)

7) May the number of traces described by the sequence diagram on Foil 27 be reduced to one by adding messages?

8) Write a sequence diagram that specifies exactly 10 traces

9) Is it possible to write a sequence diagram describing exactly five traces using only the seq-operator?