Verification of queues and FIFO properties

The specifications are based on the following basic event types:

• enq(val): value val has been inserted in the queue;
• deq(val): value val has been removed from the queue;
• peek(val): value val is retrieved but not removed from the head of the queue.

Randomized queues with enqueue and dequeue

// queue1: single random queue with enqueue and dequeue 
Main = Queue!; 
Queue = {let val; enq(val) (deq(val) | Queue)}; 

Randomized queues with enqueue, dequeue and peek

Exercise

Show that the following extension of queue1, that should verify also peek, is not correct. (see the solution)

// queue2: incorrect specification!
Main = Queue!; 
Queue = {let val; enq(val) (peek(val)*deq(val) | Queue)}; 

Exercise

Fix the incorrect version of queue2 by following the approach ‘by decomposition’, that is, by imposing a constraint with the intersection operator. (see the solution)

Randomized queues with no repetitions, enqueue and dequeue

// queue3: single random queue with no repetitions, enqueue and dequeue
Main = Queue!; 
Queue = {let val; enq(val) (enq(val)* deq(val) | Queue)}; 

Randomized queues with no repetitions, enqueue, dequeue and peek

Exercise

Extend specification queue3 to verify peek. (see the solution)

FIFO queues with enqueue and dequeue

// queue5: single FIFO queue with enqueue and dequeue 

deq matches deq(_);

Main = Queue!; 
Queue={let val; enq(val) ((deq|Queue)/\(deq>>deq(val) all))};

FIFO queues with enqueue, dequeue and peek

Exercise

Extend specification queue5 to verify peek. (see the solution)

Hint: the pattern used for queue2 and queue4 does not work!

FIFO queues with no repetitions, enqueue and dequeue

Exercise

Extend specification queue3 to verify FIFO queues with no repetitions, enqueue and dequeue. (see the solution)