Dafny 中使用全称量词的断言存在问题

Question

我在 Dafny 中问了一个关于“forall predicates”的问题，但按照答案的建议我没有得到我想要的。

问题如下：我有一个“对所有 i :: 0 <= i < |s| ==> P(i,s) 的断言”，其中 s 是一个具有指定值的有限序列，P 是我的代码中定义的谓词。 Dafny 无法验证断言（可能是由于它使用的触发器），但它可以验证每个“断言 P(0,s)”“断言 P(1,s)”...“断言 P(|s |- 1，s)”。由于 s 可能非常大，因此编写所有断言并不是合适的解决方案。 我想对许多序列系统地执行此操作，请问有人可以告诉我是否有办法帮助 Dafny 执行此操作？是否可以通过触发器强制 Dafny 检查有限域 forall？

Answer 1

由于单独

P(i, s)

对于所有

i

以便

0 <= i < |s|

进行验证。

一个建议是写下下面的内容，看看它是否验证

   forall i | 0 <= i < |s| ensures P(i, s) {}
   assert forall i :: 0 <= i < |s| ==> P(i, s);

以下是演示上述内容的示例

predicate NotTrue(p: nat)
{ 
    if p == 0 then false
    else NotTrue(p-1)
}

ghost predicate Q(i: nat, s: seq<nat>)
    requires 0 <= i < |s|
{
    forall k : nat :: 0 <= k <= s[i] ==> !NotTrue(k)
}

lemma M(s: seq<nat>)
   requires |s| > 0
   requires forall i :: 0 <= i < |s| ==> s[i] <= 2
{
   assert Q(0, s);
   assert Q(|s|-1, s);
   forall i | 0 <= i < |s| ensures Q(i, s) {}
   assert forall i :: 0 <= i < |s| ==> Q(i, s);
}

如果没有

forall i | 0 <= i < |s| ensures Q(i, s) {}

行，则此

assert forall i :: 0 <= i < |s| ==> Q(i, s);

无法验证。