0

我目前正在尝试学习如何使用 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]toout[-1]是可读的，out[0]toout[length-1]是可写的。PLCC 第 210 页讲述了一个条件array_at_range，但它似乎在 VST 1.5 中不可用。我怎样才能做到这一点？

4

1 回答 1

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/verif_revarray.v 中进行了说明；特别注意该文件中的 reverse_Inv。

于 2015-08-10T13:08:02.077 回答