Doubly-linked lists, verified¶
Verifying the doubly-linked list operations requires a few extra annotations.
The basic definitions are unchanged from the associated testing chapter, except that as usual we need some boilerplate for allocation and deallocation.
extern struct dllist *malloc__dllist();
/*@ spec malloc__dllist();
requires true;
ensures take R = W<struct dllist>(return);
!ptr_eq(return,NULL);
@*/
extern void free__dllist (struct dllist *p);
/*@ spec free__dllist(pointer p);
requires take R = W<struct dllist>(p);
ensures true;
@*/
Singleton¶
The singleton function can be verified by CN with no additional annotations.
#include "./headers.verif.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 a version with just the pre- and
post-condition as in the testing version of this chapter:
#include "./headers.verif.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;
}
}
Exercise: Before reading on, see if you can figure out what annotations need to be added to the body of the function to make CN accept it.
Here is the fully annotated version:
#include "./headers.verif.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 {
/*@ 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;
}
}
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 Take_Left
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
Take_Right predicate. Note that we have to go one more node forward
to make sure that everything past n->next is still RW at the end of
the function.
Remove¶
Here is the remove operation with just its specification:
#include "./headers.verif.h"
#include "./dllist_and_int.verif.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 = 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;
}
Exercise: Before reading on, see if you can figure out what annotations are needed to make CN happy.
Here is the fully annotated version of remove:
#include "./headers.verif.h"
#include "./dllist_and_int.verif.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 = 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) {
/*@ 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;
}
The annotations in the function body are similar to in the add
function. Both of these split_case annotations are needed to unpack
the Take_Right and Take_Left 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 and verifying their specifications.
Exercise: For extra practice, try coming up with one or two variations on the DlList data structure itself (there are many!).