Imperative queues¶
A queue is a linked list with constant-time operations for adding things to one end (the "back") and removing them from the other (the "front"). Here are the C type definitions:
struct queue {
struct queue_cell* front;
struct queue_cell* back;
};
struct queue_cell {
int first;
struct queue_cell* next;
};
A queue consists of a pair of pointers, one pointing to the front
element, which is the first in a linked list of queue_cells,
the other pointing directly to the last cell in this list. If the
queue is empty, both pointers are NULL.
Abstractly, a queue just represents a list, so we can reuse the List
type from the list examples earlier in the tutorial as the result type
when we take a queue from the heap.
/*@
predicate (datatype List) QueuePtr_At (pointer q) {
take Q = RW<struct queue>(q);
assert ( (is_null(Q.front) && is_null(Q.back))
|| (!is_null(Q.front) && !is_null(Q.back)));
take L = QueueFB(Q.front, Q.back);
return L;
}
@*/
Given a pointer to a queue struct, this predicate grabs ownership
of the structthen hands off to an
auxiliary predicate QueueFB. Note that QueuePtr_At returns a
List -- that is, the abstract view of a queue heap structure is
simply the sequence of elements that it contains. The difference
between a queue and a singly or doubly linked list is simply one of
concrete representation.
QueueFB is where the interesting part starts. Conceptually,
it is part of QueuePtr_At, but CN currently allows
conditional expressions only at the beginning of predicate
definitions, not after a take, so we need to make a separate
auxiliary predicate.
/*@
predicate (datatype List) QueueFB (pointer front, pointer back) {
if (is_null(front)) {
return Nil{};
} else {
take B = RW<struct queue_cell>(back);
assert (is_null(B.next));
assert (ptr_eq(front, back) || !addr_eq(front, back));
take L = QueueAux (front, back);
return Snoc(L, B.first);
}
}
@*/
First, we case on whether the front of the queue is NULL. If so,
then the queue is empty and we return the empty sequence.
If the queue is not empty, we need to walk down the linked list of
elements and gather up all their values into a sequence. But we must
treat the last element of the queue specially, for two reasons.
First, since the push operation is going to follow the back
pointer directly to the last list cell without traversing all the
others, we need to take that element now rather than waiting to
get to it at the end of the recursion starting from the front.
Second, and relatedly, there will be two pointers to this final list
cell -- one from the back field and one from the next field of
the second to last cell (or the front pointer, if there is only
one cell in the list), and we need to be careful not to take this
cell twice.
Accordingly, we begin by take-ing the tail cell and passing it
separately to the QueueAux predicate, which has the job of
walking down the cells from the front and gathering all the rest of
them into a sequence. We take the result from QueueAux and
Snoc on the very last element.
Finally, the QueueAux predicate recurses down the list of
cells and returns a list of their contents.
/*@
predicate (datatype List) QueueAux (pointer f, pointer b) {
if (ptr_eq(f,b)) {
return Nil{};
} else {
take F = RW<struct queue_cell>(f);
assert (!is_null(F.next));
assert (ptr_eq(F.next, b) || !addr_eq(F.next, b));
take B = QueueAux(F.next, b);
return Cons{Head: F.first, Tail: B};
}
}
@*/
Its first argument (f) starts out at front and progresses
through the queue on recursive calls; its b argument is always a
pointer to the very last cell.
When f and b are equal, we have reached the last cell and
there is nothing to do. We don't even have to build a singleton
list: that's going to happen one level up, in QueueFB.
Otherwise, we take the fields of the f, make a recursive
call to QueueAux to process the rest of the cells, and cons the
first field of this cell onto the resulting sequence before
returning it. Again, we need to help the CN verifier by explicitly
informing it of the invariant that we know, that F.next cannot be
null if f and b are different.
To make all this work, we also need a bit of boilerplate: just as with linked lists, we need to be able to allocate and deallocate queues and queue cells. There are no interesting novelties here.
#include "../cn_malloc.h"
struct queue *malloc__queue()
/*@ ensures take R = W<struct queue>(return); @*/
{
return cn_malloc(sizeof(struct queue));
}
void free__queue (struct queue *p)
/*@ requires take P = W<struct queue>(p); @*/
{
cn_free_sized(p, sizeof(struct queue));
}
struct queue_cell *malloc__queue_cell()
/*@ ensures take R = W<struct queue_cell>(return); @*/
{
return cn_malloc(sizeof(struct queue_cell));
}
void free__queue_cell (struct queue_cell *p)
/*@ requires take P = W<struct queue_cell>(p); @*/
{
cn_free_sized(p, sizeof(struct queue_cell));
}
Exercises¶
Exercise: The function for creating an empty queue just needs to set both of its fields to NULL. See if you can fill in its specification.
#include "./headers.test.h"
struct queue* empty_queue ()
{
struct queue *p = malloc__queue();
p->front = 0;
p->back = 0;
return p;
}
Exercise: The push and pop operations are more involved. Let's look
at push first. Here's the unannotated C code.
#include "./headers.test.h"
void push_queue (int x, struct queue *q)
{
struct queue_cell *c = malloc__queue_cell();
c->first = x;
c->next = 0;
if (q->back == 0) {
q->front = c;
q->back = c;
} else {
struct queue_cell *oldback = q->back;
q->back->next = c;
q->back = c;
}
return;
}
Write down a reasonable top-level specification for this function and test that the code satisfies it.
Exercise: Now let's look at the pop operation. Here is the un-annotated
version:
#include "./headers.verif.h"
int pop_queue (struct queue *q)
{
struct queue_cell* h = q->front;
if (h == q->back) {
int x = h->first;
free_queue_cell(h);
q->front = 0;
q->back = 0;
return x;
} else {
int x = h->first;
q->front = h->next;
free_queue_cell(h);
return x;
}
}
Write down a top-level specification and test that the code satisfies it.