Dafny谓词既非真也非假

Question

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

Answer 1

达夫尼并不是说这些说法是错误的，而是说它不能证明这些说法成立。如果你给予它更多的帮助，那么它将证明那是正确的：

predicate sorted(s: seq<int>)
{
  forall j, k :: 0 <= j < k < |s| ==> s[j] <= s[k]
}

lemma SortedTest()
{
  var a := [1, 3, 2];
  assert a[0] == 1 && a[1] == 3 && a[2] == 2;
  assert  sorted(a);
  assert !sorted(a);
}