0

VST 版本 1.7。

当我尝试在函数调用中使用它们时，我遇到了一个问题，即 coq 无法识别本地声明的变量。我有代码：

void deSignArray(int bits[], int invKey, int size)
{
int i = 0;
while (i < size) {
int bit = bits[i];
int ans = deSignInt(bit, invKey);
bits[i] = ans;
i++;
}
}

使用 coq 类型位：列表 Z，invKey：Z，大小：Z。

我成功地完成了 bit = bits[i] 步骤，但是当我尝试使用

forward_call((Int.repr bit), (Int.repr invKey)).

该步骤失败，在环境中找不到位。我尝试使用

forward_call(_bit, (Int.repr invKey)).

因为 _bit 出现在 LOCAL 子句中，但这提供了类型不匹配，因为 _bit 是 ident 类型而不是 int 或 Z 类型。我想知道我应该如何使用我本地定义的值来调用其他函数，任何帮助将不胜感激。

4

1 回答 1

1

在您的情况下，您提供给 forward_call 的参数（Int.repr bit，Int.repr invKey）必须是 Coq 值。在您的情况下，如果（在 forward_call 时）您的 Coq 证明目标中的变量“bit”和“invKey”高于该行，那么这应该有效。

您将如何使这些变量高于该线？如果您的函数前置条件的 LOCALS 部分包含 (temp _invKey (Vint (Int.repr invkey)))，那么您应该在行上方有 invKey。然后，在继续执行加载语句 (bit = bits[i]) 之后，您当前的证明目标的先决条件应该有一个形式为 (temp _bit something-or-other) 的 LOCALS，它就是那个或其他的东西你应该使用而不是“位”。

于 2016-11-14T13:13:16.983 回答