Dafny 文档没有使用“存在”量词。
method Main() {
assert (exists n: int :: n > 1);
}
这会出现断言错误
以下作品：
predicate dummy(n: int) {true}
method Main() {
assert dummy(2);
assert (exists n : int {:trigger dummy(n)} :: n > 1);
}
您可以更换dummy(2) with dummy(m)对于任意整数m > 1.
这个答案不太好，因为我无法确切地告诉你为什么上面的方法有效。但是，有关触发器的更多信息，您可以阅读this https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those.
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
