Introduction

Each of the following questions requires the construction of a refinement within Event-B. In each question, you should provide an appropriate invariant, linking the state of the machine being refined to the state of the refinement. You should also make sure that the events of the refinement reflect the events of the machine being refined. In questions 1 and 2, the linking invariant and context of the refinement is provided, so you only have to define the events.

Question 1

In the project Progress.zip, the machine Progress tracks the career progress of employees by partitioning them into three sets. It should be refined to maintain a partial function from employees to their employment status as described in the template ProgressR.

Question 2

In the project Papers.zip, refine the machine Papers so that the set of houses is maintained by a partial function as described in the template PapersR.

Question 3

A stack is a last-in-first-out queue, which allows elements to be pushed onto the top of the stack, or popped from the top of the stack. Such a stack is specified in the project Stack.zip in the machine Stack. You should give a refinement for this machine. Your refinement should use an array to record the elements of the stack in order, but it should not use a separate variable to keep track of the top of the stack.

Question 4

In the project Buffer.zip, provide a refinement of the machine Buffer, which implements a first-in-first-out queue.

You should achieve this by using an array a :0..maxsize-1 --> ELEMENT to keep track of the contents of the buffer. You will also need some other state variables: f, to keep track of the next element to be output, b, to keep track of the point beyond the end of the buffer (i.e. where the next input will be placed), and you should also track the number of elements in the buffer.

The contents of the buffer will correspond to the elements of the array between f and b (allowing for wrap-around if b < f because of arithmetic modulo maxsize).

For example, with maxsize = 10, the buffer containing 3,5,4 and 8 may correspond to the array [0,0,0,0,3,5,4,8,0,0] with f = 4 and b = 8. It may also be represented by [4,8,0,0,0,0,0,0,3,5] with f = 8 and b = 2.

The linking invariant will thus link the buffer and the array a as follows:

!n.n:dom(buffer) => buffer(n)=a(n mod maxsize)

It will also have to relate f and b to front and back.