如何解决使用多重集触发 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条件中。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。