Dafny-Prädikat weder wahr noch falsch

Question

Wie kann ein Dafny-Prädikat weder wahr noch falsch sein?

Dies:

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

Erzeugt doppelte Behauptung Verletzungen:

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 sagt nicht, dass die Behauptungen falsch sind, es zu sagen, dass es nicht beweisen, dass sie halten. Wenn Sie es ein wenig mehr Hilfe geben, dann wird es beweisen, dass das wahr ist:

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