使用多重集触发 Dafny

问题描述

这个引理验证，但它引发警告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。我会努力的。

解决方法

这是转换程序的一种方法，以便没有触发警告。

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,f);
       forall j | c <= j <= f
        ensures b[j] >= x
       {
        assert b[j] in SeqRangeToMultiSet(b,f);
       }
}

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

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