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 O(1) 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 annotations for some of the functions that manipulate doubly linked lists.

First, here is the C type definition:

exercises/dll/c_types.h

struct dllist {
  int data;  
  struct dllist* prev;
  struct dllist* next;
};

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.

exercises/dll/cn_types.h

/*@
datatype Dll {
    Empty_Dll    {},
    Nonempty_Dll {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.

exercises/dll/predicates.h

/*@
predicate (datatype Dll) Dll_at (pointer p) {
    if (is_null(p)) {
        return Empty_Dll{};
    } else {
        take n = Owned<struct dllist>(p);
        take L = Own_Backwards(n.prev, p, n);
        take R = Own_Forwards(n.next, p, n);
        return Nonempty_Dll{left: L, curr: n, right: R};
    }
}

predicate (datatype List) Own_Forwards (pointer p, 
                                        pointer prev_pointer, 
                                        struct dllist prev_dllist) {
    if (is_null(p)) {
        return Nil{};
    } else {
        take P = Owned<struct dllist>(p);
        assert (ptr_eq(P.prev, prev_pointer));
        assert(ptr_eq(prev_dllist.next, p));
        take T = Own_Forwards(P.next, p, P);
        return Cons{Head: P.data, Tail: T};
    }
}

predicate (datatype List) Own_Backwards (pointer p, 
                                         pointer next_pointer, 
                                         struct dllist next_dllist) {
    if (is_null(p)) {
        return Nil{};
    } else {
        take P = Owned<struct dllist>(p);
        assert (ptr_eq(P.next, next_pointer));
        assert(ptr_eq(next_dllist.prev, p));
        take T = Own_Backwards(P.prev, p, P);
        return Cons{Head: P.data, Tail: T};
    }
}
@*/

Note that Dll_at takes ownership of the node passed in, and then calls Own_Backwards and Own_Forwards, which recursively take ownership of the rest of the list.

Also, notice that Own_Forwards and Own_Backwards 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 Own_Forwards 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 Dll datatype. This will make the specifications easier to write.

exercises/dll/getters.h

/*@
function (datatype List) Right_Sublist (datatype Dll L) {
    match L {
        Empty_Dll {} => { Nil{} }
        Nonempty_Dll {left: _, curr: _, right: r} => { r }
    }
}

function (datatype List) Left_Sublist (datatype Dll L) {
    match L {
        Empty_Dll {} => { Nil {} }
        Nonempty_Dll {left: l, curr: _, right: _} => { l }
    }
}

function (struct dllist) Node (datatype Dll L) {
    match L {
        Empty_Dll {} => {  default<struct dllist> }
        Nonempty_Dll {left: _, curr: n, right: _} => { n }
    }
}
@*/

We also need some boilerplate for allocation and deallocation.

exercises/dll/malloc_free.h

extern struct dllist *malloc__dllist();
/*@ spec malloc__dllist();
    requires true;
    ensures take R = Block<struct dllist>(return);
            !ptr_eq(return,NULL);
@*/ 

extern void free__dllist (struct dllist *p);
/*@ spec free__dllist(pointer p);
    requires take R = Block<struct dllist>(p);
    ensures true;
@*/

For convenience, we gather all of these files into a single header file.

exercises/dll/headers.h

#include "../list/headers.h"
#include "../list/append.h"
#include "../list/rev.h"
#include "./c_types.h"
#include "./cn_types.h"
#include "./getters.h"
#include "./malloc_free.h"
#include "./predicates.h"

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).

exercises/dll/singleton.c

#include "./headers.h"

struct dllist *singleton(int element)
/*@ ensures take Ret = Dll_at(return);
        Ret == Nonempty_Dll {
                 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;
}

The add and remove functions are where it gets a little tricker. Let's start with add. Here is the unannotated version:

exercises/dll/add_orig.broken.c

#include "./headers.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 and what other are needed.

Now, here is the annotated version of the add operation:

exercises/dll/add.c

#include "./headers.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 = Dll_at(n);
    ensures  take After = Dll_at(return);
             is_null(n) ? 
                After == Nonempty_Dll { 
                           left: Nil{}, 
                           curr: Node(After), 
                           right: Nil{}}
              : After == Nonempty_Dll { 
                           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 { 
        /*@ split_case(is_null(n->prev)); @*/
        new_dllist->next = n->next;
        new_dllist->prev = n;

        if (n->next != 0) {
            /*@ split_case(is_null(n->next->next)); @*/
            n->next->prev = new_dllist;
        }

        n->next = new_dllist;
        return new_dllist;
    }
}

First, let's look at the pre- and post-conditions. The requires clause is straightforward. We need to own the list centered around the node that n points to. Before is a Dll 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 Dll 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 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.

Now, let's look at the annotations in the function body. CN can figure out the empty list case for itself, but it needs some help with the non-empty list case. The split_case on is_null(n->prev) tells CN to unpack the Own_Backwards predicate. Without this annotation, CN cannot reason that we didn't lose the left half of the list before we return, and will claim we are missing a resource for returning. The split_case on is_null(n->next->next) is similar, but for unpacking the Own_Forwards predicate. Note that we have to go one more node forward to make sure that everything past n->next is still owned at the end of the function.

Now 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.

exercises/dll/dllist_and_int.h

struct dllist_and_int {
  struct dllist* dllist;
  int data;
};

extern struct dllist_and_int *malloc__dllist_and_int();
/*@ spec malloc__dllist_and_int();
    requires true;
    ensures take R = Block<struct dllist_and_int>(return);
            !ptr_eq(return,NULL);
@*/ 

extern void free__dllist_and_int (struct dllist_and_int *p);
/*@ spec free__dllist_and_int(pointer p);
    requires take R = Block<struct dllist_and_int>(p);
    ensures true;
@*/

Now we can look at the code for the remove operation. Here is the un-annotated version:

exercises/dll/remove_orig.broken.c

#include "./headers.h"
#include "./dllist_and_int.h"

// removes 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(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 and what annotations are needed.

Now, here is the fully annotated version of the remove operation:

exercises/dll/remove.c

#include "./headers.h"
#include "./dllist_and_int.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(struct dllist *n)
/*@ requires !is_null(n);
             take Before = Dll_at(n);
             let Del = Node(Before);
    ensures  take Ret = Owned<struct dllist_and_int>(return);
             take After = Dll_at(Ret.dllist);
             Ret.data == Del.data;
             (is_null(Del.prev) && is_null(Del.next)) 
               ? After == Empty_Dll{}
               : (!is_null(Del.next) ? 
                    After == Nonempty_Dll {left: Left_Sublist(Before), 
                                           curr: Node(After), 
                                           right: Tl(Right_Sublist(Before))}
                   : After == Nonempty_Dll {left: Tl(Left_Sublist(Before)), 
                                            curr: Node(After), 
                                            right: Right_Sublist(Before)});
@*/
{
    struct dllist *temp = 0;
    if (n->prev != 0) {
        /*@ split_case(is_null(n->prev->prev)); @*/
        n->prev->next = n->next;
        temp = n->prev;
    }
    if (n->next != 0) {
        /*@ split_case(is_null(n->next->next)); @*/
        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;
}

First, 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 Dll 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 Dll that the node is part of. Here, After refers to the Dll 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.prev and del.next are null. In this case, we are removing the only node in the list, so the resulting list will be empty. The else branch of this conditional contains its own conditional.

• For the following conditional, the guard checks if 'del.prev' is not null. This means that the returned node is del.next, regardless of whether or not del.prev is null. If this is the case, After is now centered around del.next, and the left part of the list is the same as before. Since del.next was previously the head of the right side, the right side loses its head in After. This is where we get After == Dll{left: Left_Sublist(Before), curr: Node(After), right: Tl(Right(Before))}.

• The final else branch is the case where del.next is null, but del.prev is not null. In this case, the returned node is del.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 in After == Dll{left: Tl(Left_Sublist(Before)), curr: Node(After), right: Right(Before)};

The annotations in the function body are similar to in the add function. Both of these split_case annotations are needed to unpack the Own_Forwards and Own_Backwards predicates. Without them, CN will not be able to reason that we didn't lose the left or right half of the list before we return and will claim we are missing a resource for returning.

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 Dll data structure itself (there are many!).