coq - 如何在 VST 工具中使用分离逻辑来描述双链接

Question

以 VST 项目中的示例为例，reverse.c 文件有一个这样的链表：

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;
}

它的分离逻辑写成：

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

其中 LS 定义为：

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

我的问题是如果我有一个双链表，如何编写其对应的分离逻辑。例如：这样的双链表：

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

那么，“”应该是什么SEP (lseg LS?? sh (map Vint contents) p nullval)？

Answer 1

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.