Dafny предикат не истинно и не false

Question

Как предикат Дафни не будет ни истинным, ни ложным?

Это:

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

Dafny не говорит о том, что утверждения являются ложными, он говорит, что он не может доказать что они держат. Если вы немного поможете, это докажет это:

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); 
}