用多重集触发 Dafny

Question

这个引理可以验证，但会引发警告 Not triggers found:

lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
       requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
       requires (forall j :: c <= j <= f ==> a[j] >= x)
       requires multiset(a[c..f+1]) == multiset(b[c..f+1])
       ensures (forall j :: c <= j <= f ==> b[j] >= x)
{

       assert (forall j :: j in multiset(a[c..f+1]) ==> j in multiset(b[c..f+1]));

}

我不知道如何实例化这个触发器（不能将它实例化为一个函数，或者我可以吗？）。有帮助吗？

编辑：也许我可以实例化一个方法 f，它接受一个数组并将其插入到一个多重集中，因此我可以触发 f(a)，但这并没有提到 i。我会努力的。

Answer 1

这是一种转换程序的方法，这样就不会有触发警告。

function SeqRangeToMultiSet(a: seq<int>, c: int, f: int): multiset<int>
  requires 0 <= c <= f + 1 <= |a|
{
  multiset(a[c..f+1])
}

lemma multisetPreservesGreater (a:seq<int>, b:seq<int>, c:int, f:int, x:int)
       requires |a|==|b| && 0 <= c <= f + 1 <= |b| 
       requires (forall j :: c <= j <= f ==> a[j] >= x)
       requires multiset(a[c..f+1]) == multiset(b[c..f+1])
       ensures (forall j :: c <= j <= f ==> b[j] >= x)
{
       assert forall j :: j in SeqRangeToMultiSet(a, c, f) ==> j in SeqRangeToMultiSet(b, c, f);
       forall j | c <= j <= f
        ensures b[j] >= x
       {
        assert b[j] in SeqRangeToMultiSet(b, c, f);
       }
}

重点是我们引入了函数SeqRangeToMultiSet来表示一个不是有效触发器的子表达式（因为它包含算术）。那么SeqRangeToMultiSet本身就可以成为触发器。

这种方法的缺点是它降低了自动化程度。您可以看到我们必须添加一个 forall 语句来证明 post 条件。原因是我们需要提一下触发器，post条件中没有出现

用多重集触发 Dafny

Trigger Dafny with multisets

triggers

theorem-proving

multiset

z3

dafny