How to describe a double link using separation logic in the VST tool

Question

As an example in the VST project, the reverse.c file has a linked list like this:

struct list {unsigned head; struct list *tail;};
unsigned sumlist (struct list *p) {
  unsigned s = 0;
  struct list *t = p;
  unsigned h;
  while (t) {
     h = t->head;
     t = t->tail;
     s = s + h;
  }
  return s;
}

and it's separation logic is wrote as:

SEP (lseg LS sh (map Vint contents) p nullval)

in which the LS is defined as:

Instance LS: listspec _list _tail (fun _ _ => emp).
Proof. eapply mk_listspec; reflexivity. Defined.

My question is if I have a double linked list, how to write its corresponding separation logic. for example: the double linked list like this:

struct list {unsigned head; struct list *prev;struct list *tail;};

so, what should be the "SEP (lseg LS?? sh (map Vint contents) p nullval)"?

score 4 · Answer 1 · answered Mar 01 '18 at 13:37

First, I would suggest using "verif_reverse2.v" instead of "verif_reverse.v". If you don't have a recent version of VST, get VST 2.0 (or get the master branch of the github repo) and look at verif_reverse2.v, and look at the description of this case study in doc/VC.pdf.

Still, that's for singly linked lists.

Googling "doubly linked list separation logic" gives this useful reference:

http://www.eecs.qmul.ac.uk/~gretay/papers/SepLogicIntro.ppt (see slide 17)

Using the Fixpoint technique shown in verif_reverse2.v, you should be able to adapt that solution.

How to describe a double link using separation logic in the VST tool

1 Answers1