2
Dafny谓词如何既不真实也不假?Dafny谓词既非真也非假
此:
predicate sorted(s: seq<int>)
{
forall j, k :: 0 <= j < k < |s| ==> s[j] <= s[k]
}
lemma SortedTest()
{
assert sorted([1, 3, 2]);
assert !sorted([1, 3, 2]);
}
产生双向断言违规:
Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
Sort.dfy(8,10): Error: assertion violation
Sort.dfy(3,2): Related location
Sort.dfy(3,43): Related location
Execution trace:
(0,0): anon0
Sort.dfy(9,9): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 2 verified, 2 errors
谢谢!这似乎是一个奇怪的暗示必须给。 :-) – Calder
这是用Dafny编码的方式来完成的。基本上Dafny通常只会自动展开一次归纳定义。所以它通常只会选择数组中最近分配的元素来实例化量词(例如,在_current_堆中分配的唯一元素),除非您做了某些事情(如我写的断言),导致其他相关元素为在当前堆的求解器电子图中。根据我的经验,它实际上更好地处理公式(通常是数组)而不是具体值(特定数组)。 – lexicalscope
有没有办法说出“我可以证明这是错误的”和“我无法证明这是正确的”之间的区别? –