Как описать двойную связь, используя логику разделения в инструменте 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

Во-первых, я бы предложил использовать "verify_reverse2.v" вместо "verify_reverse.v". Если у вас нет последней версии VST, получите VST 2.0 (или получите основную ветку репозитория github) и посмотрите на verify_reverse2.v, а также посмотрите описание этого примера в doc/VC.pdf.

Тем не менее, это для односвязных списков.

Поиск в Google "логики разделения двусвязных списков" дает полезную ссылку:

http://www.eecs.qmul.ac.uk/~gretay/papers/SepLogicIntro.ppt(см. слайд 17)

Используя технику Fixpoint, показанную в verify_reverse2.v, вы сможете адаптировать это решение.