dafny - テストデータに直面したときにDafny量指定子がインスタンス化されない

Question

文字の配列に重複が含まれているかどうかを判断する述語をdafnyで作成しようとしています。最終的には次のように何かをテストする必要があります。要素が 2 つ未満の場合は無視してください

predicate noDuplicates (a:array<char>)
requires a!= null
reads a
{
forall j,k:: (0<=j<a.Length && 0<=k<a.Length) ==> ((a[j]==a[k]) ==> (j==k))
}

ただし、次のテストを実行すると、アサーションに失敗します。なぜこうなった？

var b: array<char> := new char[5];
b[0], b[1], b[2], b[3], b[4] := 't', 'e', 's', 't', 's';
assert noDuplicates(b) == false;