如何解决要求在a中声明a [0]
我目前正在学习dafny,并遇到了一个非常奇怪的断言要求:
method M (a : seq<int>,acc : seq<int>)
requires |a| > 0
requires forall va,vacc :: va in a && vacc in acc ==> vacc <= va
{
assert forall vacc :: vacc in acc ==> vacc <= a[0];
}
上面的代码在断言时失败,但是如果我添加assert a[0] in a
,它可以验证吗?
为什么会这样呢?肯定在所有情况下|a| > 0
都是不可变的,a[0] in a
seq
成立?
(任何样式指南建议也将不胜感激:))
解决方法
这与“触发器”有关。
简短的答案是,除非您手动“提及” a[0]
,否则Dafny将无法利用量化的requires
子句。您提到a[0]
的方式并不重要,只要您提及它即可。这就是为什么即使琐碎的断言似乎并没有在逻辑上添加任何内容的原因,它仍然起作用的原因:只是因为它提到了a[0]
。
有关更多信息,请参见:
- FAQ qustion
- this answer“什么是触发器?”
- this answer关于“找不到要触发的字词”
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。