Doubly-linked lists¶
A doubly linked list is a linked list where each node has a pointer to both the next node and the previous node. This allows for constant-time operations for adding or removing nodes anywhere in the list.
Because of all the sharing in this data structure, the separation reasoning is a bit tricky. We'll give you the core definitions and then invite you to help fill in the specifications for some of the functions that manipulate doubly linked lists.
Types¶
First, here is the C type definition:
The idea behind the representation of this list is that we don't keep
track of the front or back, but rather we take any node in the list
and have a sequence to the left and to the right of that node. The left
and right are from the point of view of the node itself, so left
is kept in reverse order. Additionally, similarly to in the
Imperative Queues example, we can reuse the List type.
/*@
datatype DlList {
Empty_DlList {},
Nonempty_DlList {datatype List left,
struct dllist curr,
datatype List right}
}
@*/
The predicate for this datatype is a bit complicated. The idea is that
we first own the node that is passed in. Then we follow all of the
prev pointers to own everything backwards from the node, and finally
all the next pointers to own everything forwards from the node, to
construct the left and right fields.
/*@
predicate (datatype DlList) DlList_at (pointer p) {
if (is_null(p)) {
return Empty_DlList{};
} else {
take n = RW<struct dllist>(p);
take L = Take_Left(n.prev, p, n);
take R = Take_Right(n.next, p, n);
return Nonempty_DlList{left: L, curr: n, right: R};
}
}
predicate (datatype List) Take_Right (pointer p,
pointer prev_pointer,
struct dllist prev_dllist) {
if (is_null(p)) {
return Nil{};
} else {
take P = RW<struct dllist>(p);
assert (ptr_eq(P.prev, prev_pointer));
assert (ptr_eq(prev_dllist.next, p));
take T = Take_Right(P.next, p, P);
return Cons{Head: P.data, Tail: T};
}
}
predicate (datatype List) Take_Left (pointer p,
pointer next_pointer,
struct dllist next_dllist) {
if (is_null(p)) {
return Nil{};
} else {
take P = RW<struct dllist>(p);
assert (ptr_eq(P.next, next_pointer));
assert (ptr_eq(next_dllist.prev, p));
take T = Take_Left(P.prev, p, P);
return Cons{Head: P.data, Tail: T};
}
}
@*/
Note that DlList_at takes ownership of the node passed in, and then
calls Take_Left and Take_Right, which recursively take
ownership of the rest of the list.
Also, notice that Take_Right and Take_Left include ptr_eq
assertions for the prev and next pointers. This is to ensure that
the nodes in the list are correctly doubly linked. For example, the
line assert (ptr_eq(n.prev, prev_pointer)); in Take_Right
ensures that the current node correctly points backward to the
previous node in the list. The line assert(ptr_eq(prev_node.next,
p)); ensures that the previous node correctly points forward to the
current node.
Before we move on to the functions that manipulate doubly linked
lists, we need to define a few "getter" functions that will allow us
to access the fields of our DlList datatype. This will make the
specifications easier to write.
/*@
function (datatype List) Right_Sublist (datatype DlList L) {
match L {
Empty_DlList {} => { Nil{} }
Nonempty_DlList {left: _, curr: _, right: r} => { r }
}
}
function (datatype List) Left_Sublist (datatype DlList L) {
match L {
Empty_DlList {} => { Nil {} }
Nonempty_DlList {left: l, curr: _, right: _} => { l }
}
}
function (struct dllist) Node (datatype DlList L) {
match L {
Empty_DlList {} => { default<struct dllist> }
Nonempty_DlList {left: _, curr: n, right: _} => { n }
}
}
@*/
We also need the usual boilerplate for allocation and deallocation.
#include "../cn_malloc.h"
struct dllist *malloc__dllist()
/*@ ensures take R = W<struct dllist>(return); @*/
{
return cn_malloc(sizeof(struct dllist));
}
void free__dllist (struct dllist *p)
/*@ requires take P = W<struct dllist>(p); @*/
{
cn_free_sized(p, sizeof(struct dllist));
}
For convenience, we gather all of these files into a single header file.
#include "../list/headers.test.h"
#include "../list/append.h"
#include "../list/rev.h"
#include "./c_types.h"
#include "./cn_types.h"
#include "./getters.h"
#include "./allocation.test.h"
#include "./predicates.h"
Singleton¶
Now we can move on to an initialization function. Since an empty list is represented as a null pointer, we will look at initializing a singleton list (or in other words, a list with only one item).
#include "./headers.test.h"
struct dllist *singleton(int element)
/*@ ensures take Ret = DlList_at(return);
Ret == Nonempty_DlList {
left: Nil{},
curr: struct dllist {prev: NULL,
data: element,
next: NULL},
right: Nil{}};
@*/
{
struct dllist *n = malloc__dllist();
n->data = element;
n->prev = 0;
n->next = 0;
return n;
}
Add¶
The add and remove functions are where it gets a little tricker.
Let's start with add. Here is the unannotated version:
#include "./headers.test.h"
// Adds after the given node and returns a pointer to the new node
struct dllist *add(int element, struct dllist *n)
{
struct dllist *new_dllist = malloc__dllist();
new_dllist->data = element;
new_dllist->prev = 0;
new_dllist->next = 0;
if (n == 0) //empty list case
{
new_dllist->prev = 0;
new_dllist->next = 0;
return new_dllist;
} else {
new_dllist->next = n->next;
new_dllist->prev = n;
if (n->next != 0) {
n->next->prev = new_dllist;
}
n->next = new_dllist;
return new_dllist;
}
}
Exercise: Before reading on, see if you can figure out what specification is appropriate.
Now, here is the annotated version of the add operation:
#include "./headers.test.h"
// Adds after the given node and returns a pointer to the new node
struct dllist *add(int element, struct dllist *n)
/*@ requires take Before = DlList_at(n);
ensures take After = DlList_at(return);
is_null(n) ?
After == Nonempty_DlList {
left: Nil{},
curr: Node(After),
right: Nil{}}
: After == Nonempty_DlList {
left: Cons {Head: Node(Before).data,
Tail: Left_Sublist(Before)},
curr: Node(After),
right: Right_Sublist(Before)};
@*/
{
struct dllist *new_dllist = malloc__dllist();
new_dllist->data = element;
new_dllist->prev = 0;
new_dllist->next = 0;
if (n == 0) //empty list case
{
new_dllist->prev = 0;
new_dllist->next = 0;
return new_dllist;
} else {
new_dllist->next = n->next;
new_dllist->prev = n;
if (n->next != 0) {
n->next->prev = new_dllist;
}
n->next = new_dllist;
return new_dllist;
}
}
The requires
clause is straightforward. We need to own the list centered around
the node that n points to. Before is a DlList
that is either empty, or it has a List to the left,
the current node that n points to, and a List to the right.
This corresponds to the state of the list when it is passed in.
In the ensures clause, we again establish ownership of the list, but
this time it is centered around the added node. This means that
After is a DlList structure similar to Before, except that the node
curr is now the created node. The old curr is pushed into the left
part of the new list. The conditional operator in the ensures clause
is saying that if the list was empty coming in, it now is a singleton
list. Otherwise, the left part of the list now has the data from
the old curr node, the new curr node is the added node, and the
right part of the list is the same as before.
Remove¶
Finally, let's look at the remove operation. Traditionally, a remove
operation for a list returns the integer that was removed. However we
also want all of our functions to return a pointer to the
list. Because of this, we define a struct that includes an int
and a node.
struct dllist_and_int {
struct dllist* dllist;
int data;
};
struct dllist_and_int *malloc__dllist_and_int()
/*@ ensures take R = W<struct dllist_and_int>(return); @*/
{
return cn_malloc(sizeof(struct dllist_and_int));
}
void free__dllist_and_int (struct dllist_and_int *p)
/*@ requires take P = W<struct dllist_and_int>(p); @*/
{
cn_free_sized(p, sizeof(struct dllist_and_int));
}
Now we can look at the code for the remove operation. Here is the un-annotated version:
#include "./headers.test.h"
#include "./dllist_and_int.test.h"
// Remove the given node from the list and returns another pointer
// to somewhere in the list, or a null pointer if the list is empty
struct dllist_and_int *remove_current(struct dllist *n)
{
struct dllist *temp = 0;
if (n->prev != 0) {
n->prev->next = n->next;
temp = n->prev;
}
if (n->next != 0) {
n->next->prev = n->prev;
temp = n->next;
}
struct dllist_and_int *pair = malloc__dllist_and_int();
pair->dllist = temp;
pair->data = n->data;
free__dllist(n);
return pair;
}
Exercise: Before reading on, see if you can figure out what specification is appropriate.
Now, here is the annotated version of remove:
#include "./headers.test.h"
#include "./dllist_and_int.test.h"
// Remove the given node from the list and returns another pointer
// to somewhere in the list, or a null pointer if the list is empty
struct dllist_and_int *remove_current(struct dllist *n)
/*@ requires !is_null(n);
take Before = DlList_at(n);
let Del = Node(Before);
ensures take Ret = RW<struct dllist_and_int>(return);
take After = DlList_at(Ret.dllist);
Ret.data == Del.data;
(is_null(Del.prev) && is_null(Del.next))
? After == Empty_DlList{}
: (!is_null(Del.next) ?
After == Nonempty_DlList {left: Left_Sublist(Before),
curr: Node(After),
right: Tl(Right_Sublist(Before))}
: After == Nonempty_DlList {left: Tl(Left_Sublist(Before)),
curr: Node(After),
right: Right_Sublist(Before)});
@*/
{
struct dllist *temp = 0;
if (n->prev != 0) {
n->prev->next = n->next;
temp = n->prev;
}
if (n->next != 0) {
n->next->prev = n->prev;
temp = n->next;
}
struct dllist_and_int *pair = malloc__dllist_and_int();
pair->dllist = temp;
pair->data = n->data;
free__dllist(n);
return pair;
}
Let's look at the pre- and post-conditions. The requires clause says that we cannot remove a node from an empty list, so the pointer passed in must not be null. Then we take ownership of the list, and we
assign the node of that list to the identifier del
to make our spec more readable. So Before refers to the DlList when the function is called, and del refers to the node that will be deleted.
Then in the ensures clause, we must take ownership
of the node_and_int struct as well as the DlList that
the node is part of. Here, After refers to the DlList
when the function returns. We ensure that the int that is returned is the value of the deleted node, as intended. Then we have a complicated nested ternary conditional that ensures that After is the same as Before except for the deleted node. Let's break down this conditional:
-
The first guard asks if both
del.prevanddel.nextare null. In this case, we are removing the only node in the list, so the resulting list will be empty. Theelsebranch of this conditional contains its own conditional. -
For the following conditional, the guard checks if
del.previs not null. This means that the returned node isdel.next, regardless of whether or notdel.previs null. If this is the case,Afteris now centered arounddel.next, and the left part of the list is the same as before. Sincedel.nextwas previously the head of the right side, the right side loses its head inAfter. This is where we getAfter == DlList{left: Left_Sublist(Before), curr: Node(After), right: Tl(Right(Before))}. -
The final
elsebranch is the case wheredel.nextis null, butdel.previs not null. In this case, the returned node isdel.prev. This branch follows the same logic as the one before it, except now we are taking the head of the left side rather than the right side. Now the right side is unchanged, and the left side is just the tail, as seen shown inAfter == DlList{left: Tl(Left_Sublist(Before)), curr: Node(After), right: Right(Before)};
Exercises¶
Exercise: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing a few of these functions and writing their specifications.
Exercise: For extra practice, try coming up with one or two
variations on the DlList data structure itself (there are many!).