如何在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

首先，我建议使用“verif_reverse2.v”而不是“verif_reverse.v”。如果您没有最新版本的VST，请获取VST 2.0（或获取github repo的主分支）并查看verif_reverse2.v，并在doc / VC.pdf中查看此案例研究的描述。

不过，那是单链表。

谷歌搜索“双链表分离逻辑”给出了这个有用的参考：

http://www.eecs.qmul.ac.uk/~gretay/papers/SepLogicIntro.ppt（见幻灯片17）

使用verif_reverse2.v中显示的Fixpoint技术，您应该能够调整该解决方案。