Диапазон массива в предварительном условии

Question

В настоящее время я пытаюсь узнать, как использовать VST. Я использую VST 1.5. У меня есть эта маленькая программа C (backref.c):

char* rbr (char* out, int length, int dist) {
  while (length-- > 0) { out[0] = out[-dist]; out++; }
  return out;
}

Мой код Coq (с тривиальными предварительными и постусловиями)

Require Import floyd.proofauto.
Require Import backref.

Local Open Scope logic.
Local Open Scope Z.

Definition rbr_spec :=
  DECLARE _rbr
    WITH sh : share, contents : Z -> int
      PRE [ _out OF (tptr tuchar), _length OF tint, _dist OF tint ]
        PROP ()
        LOCAL ()
        SEP ()
      POST [tptr tuchar] local(fun _ => True).

В качестве предварительного условия я хотел бы сказать, что out[-dist] в out[-1] читаемы и out[0] в out[length-1] доступны для записи. PLCC стр. 210 рассказывает о состоянии array_at_range, но он не доступен в VST 1.5. Как я могу это сделать?

Answer 1

Вы можете использовать array_at. Но поскольку две разные части вашего массива имеют разные доли владения, вам придется описать их как два разных сегмента массива.

Что-то вроде:

p: val  (* base address of array *)
v1: list val  (* contents of array segment 1 *)
v2: list val  (* contents of array segment 2 *)
sh: share (* readable *)
sh': share (* writable *)

SEP (`(array_at sh tint nil (-dist) (-1) v1 p);
     `(array_at sh' tint nil 0 (length-1) v2 p))

Но это сложнее, чем это, потому что это исключает описание части ниже (-dist) и выше (length-1).

Возможно, вам не нужна полная общность различных долей владения для частей вашего массива; Вы можете подумать, зачем клиенту вашей функции это нужно? В этом случае будет проще иметь только один сегмент массива, "значением" которого является объединение нескольких списков. Это проиллюстрировано в примере progs / verify_revarray.v; обратите особое внимание на reverse_Inv в этом файле.