Определение правильного инварианта l oop при добавлении в связанный список с проверяемым C - PullRequest
Новая
       67

Определение правильного инварианта l oop при добавлении в связанный список с проверяемым C

1 голос
/ 13 июля 2020

Я работаю над пятым бета-модулем основ программного обеспечения, который охватывает проверяемые C. Я нахожусь на последней части, которая связана с операциями на карте ha sh (что требует операций со связанным списком).

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 равно нулю, идущему в l oop, но тогда гарантированно будет иметь значение, если оно зацикливается. Модуль SPE c дает следующее: 

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).

Все упражнение зависит от правильного инварианта l oop. Это была моя попытка 

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)
)).

С этим я могу добиться определенного c прогресса, но я застрял на обработке: прямо сейчас в предложении 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)

Тогда, конечно, это должно быть нулевое значение. Но значение, которое у нас есть, это data_at Ews (tptr tcell) vret r0' ...

Так что я не знаю. Я почти уверен, что мне нужно уточнить свой инвариант, но не знаю, как это сделать! Буду признателен за любые указатели.

1 Ответ

2 голосов
/ 13 июля 2020

Давайте сосредоточимся на предложении 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), поэтому вы можете спросить себя, это ли вы имели в виду?

Во-вторых, подумайте о своем маге c -жезл listboxrep al' r0' -* .... В первом пункте вашего ПВЗС говорится: «Сейчас у меня listboxrep al' r0'». Выражение палочки говорит: «Я могу заполнить отверстие r0' точно списком al'. Но list-incr собирается изменить содержимое отверстия. Так что вам не нужно точно al' в ( слева от) волшебной c палочки, вам нужно какое-то универсально определенное количественное значение-список, которое вы можете заполнить позже.

...