CSSE3100/7100 Reasoning about Programs
Week 10 Exercises
Exercise 10.1.
A unique number allocator is required to allocate unique thread ids in an operating system. The specification of a class for the allocator is given below. (Note that the notation x !in s means x is not a member of set s, and s + t is the union of sets s and t.)
class UniqueNumberAllocator {
ghost var used: set
ghost predicate Valid( )
reads this
constructor ( )
ensures Valid( ) && used == {}
method Allocate( ) returns (n: nat)
requires Valid( )
modifies this
ensures Valid( ) && n !in old(used) && used == old(used) + {n}
method Reset( )
requires Valid( )
modifies this
ensures Valid( ) && used == {}
}
Implement the class using a single variable, next, which holds the next number to allocate. next should initially be 0 and increment on each call to Allocate.
Hint: Use a quantifier to express the abstraction relation.
Exercise 10.2.
The classes CoffeeMaker1.dfy and CoffeeMaker2.dfy developed in last week's lectures are on the Learning Resources page of Blackboard (under Week 9).
Add ChangeGrinder and InstallCustomGrinder methods to CoffeeMaker2 based on those in CoffeeMaker1, but updated to reflect the fact that Grinder is a composite object.
Challenge: Specify and implement a method for CoffeeMaker1 that removes and returns the grinder of a coffee maker, replacing it with a new one that the method allocates. Make sure your specification allows the following test harness to be verified:
method RemoveGrinderHarness( ) {
var cm := new CoffeeMaker( );
var grinder := cm.RemoveGrinder( );
cm.Restock( );
grinder.AddBeans( );
}
Exercise 10.3.
A bounded queue is a sequence of up to N elements (N > 0) where users can insert elements one at a time, and then remove them one at a time in the same order that they were inserted. For example, if the user inserted the element A, then B, then C, they would first remove A, then B, and so on.
One way to implement a bounded queue is with a circular array. A circular array consists of an array and two pointers, wr and rd, to array indicies. Elements are inserted (i.e., written) at array index, wr, and removed (i.e., read) at array index, rd. That is, wr denotes the first empty space in the array (if any), and rd denotes the first full space (if any).
Below are two examples of this implementation at some time during its execution. Note that when wr reaches the end of the array, another insertion will make it wrap back to the start. Therefore, wr can be less than rd as in the second example.
When wr == rd the queue is either empty or full. An additional Boolean variable empty is used to denote whether it is empty or full.
Initially, wr and rd are both 0 and empty is true.
(a) Provide the abstract and concrete state variables for the above design of a bounded queue.
(b) Provide the class invariant as a ghost predicate Valid().
(c) Provide specifications and implementations for the constructor and the methods Insert, which inserts an element into the bounded queue, and Remove, which removes an element from the bounded queue.