使用多组触发 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 语句来证明后置条件。原因是我们需要提及触发器，它不会出现在后置条件中。