1

我正在开发涵盖可验证 C 的 beta 5 软件基础模块。我在最后一部分，这与哈希映射上的操作有关（这需要对链表进行操作）。

https://www.cs.princeton.edu/~appel/vc/vc-0.9.5/Verif_hash.html

我有点坚持body_incr_list。

正在验证的代码：

void incr_list (struct cell **r0, char *s) {
  struct cell *p, **r;
  for(r=r0; ; r=&p->next) {
    p = *r;
    if (!p) { *r = new_cell(s,1,NULL); return; }
    if (strcmp(p->key, s)==0) {p->count++; return;}
  }
}

这做了一些新的事情......一个指针的指针，以及进入循环的 p 为 null 的事实，但如果它循环，则保证有一个值。该模块给出的规范是：

Definition incr_list_spec : ident × funspec :=
 DECLARE _incr_list
 WITH r0: val, al: list (list byte × Z), s: val,
      sigma : list byte, gv: globals
 PRE [ _r0 OF tptr (tptr tcell), _s OF tptr tschar ]
    PROP (list_get sigma al < Int.max_unsigned)
    LOCAL (temp _r0 r0; temp _s s; gvars gv)
    SEP (listboxrep al r0; cstring Ews sigma s; mem_mgr gv)
 POST [ tvoid ]
      PROP ( ) LOCAL ()
      SEP (listboxrep (list_incr sigma al) r0;
           cstring Ews sigma s; mem_mgr gv).

整个练习取决于适当的循环不变量。这是我的尝试

forward_loop (EX al':list (list byte * Z), EX r0': val,
PROP ()
LOCAL (temp _r r0'; temp _r0 r0; temp _s s; gvars gv)
SEP (
  listboxrep al' r0';
  cstring Ews sigma s;
  mem_mgr gv;
  listboxrep al' r0' -* (ALL sigma:list byte, listrep (list_incr sigma []) nullval -* listboxrep (list_incr sigma al) r0)
)).

有了这个，我能够取得一些基本进展，但我陷入了以下处理：

    if (!p) { *r = new_cell(s,1,NULL); return; }

原因是现在在 SEP 子句中，我有listboxrep al' r0'，但是为了让它越过这条线

    p = *r;

我需要把它展开成data_at Ews (tptr tcell) p r0' * listrep al' p. 同样，这不是一个大问题，但在 p 为 null 并且它创建新单元格 ( *r = new_cell(s,1,NULL); return;) 的情况下，我得到了一个我不知道是否可以解决的证明目标。

这是因为data_at Ews (tptr tcell) p r0'被转换成data_at Ews (tptr tcell) vret r0'，但我们仍然只是有listrep al' p，没有listrep al' vret。虽然在这种情况下，al' 很可能是 []，这意味着我们有listrep [] p，尽管我不确定可以用它做什么。如果我遵循这一点，我最终会得到以下蕴涵：

(list_cell sigma 1 (Vint (Int.repr 0)) vret *
 data_at Ews (tptr tcell) vret r0' *
 ((EX p : val, data_at Ews (tptr tcell) p r0' * (!! (p = nullval) && emp)) -*
  (ALL sigma0 : list byte,
   (EX y : val, list_cell sigma0 1 y nullval * (!! (y = nullval) && emp)) -*
   listboxrep (list_incr sigma0 al) r0)))%logic
|-- listboxrep (list_incr sigma al) r0

这让我相信我的不变量是不正确的......例如，如果我进行调整以将 p 设置为

EX p : val, data_at Ews (tptr tcell) p r0' * (!! (p = nullval) && emp)

那么它当然需要为nullval。但我们拥有的价值是data_at Ews (tptr tcell) vret r0'......

所以我不知道。我很确定我需要改进我的不变量，但不知道如何！将不胜感激任何指针。

4

1 回答 1

2

让我们关注您提出的不变量的 SEP 子句：

SEP (
 listboxrep al' r0';
 cstring Ews sigma s;
 mem_mgr gv;
 listboxrep al' r0' -* (ALL sigma:list byte, listrep (list_incr sigma []) nullval -* listboxrep (list_incr sigma al) r0)
)).

首先，表达式listrep (list_incr sigma []) nullval等价于(list_incr sigma [] = nil && emp)，所以你可能会问自己，这就是你的意思吗？

其次，想想你的魔杖， listboxrep al' r0' -* ...。您的 SEP 的第一条说，“现在我有listboxrep al' r0'”。wand-expression 说：“我可以r0'用 list 填满这个洞al'。但是 list-incr 会修改这个洞的内容。所以你不希望正好al'在魔杖的（左侧），你想要一些普遍量化的列表值，您可以稍后填写。

于 2020-07-13T12:01:23.227 回答