Датчик 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; 

Answer 1

Я думаю, что проблема в том, что в графе решателя для dafny нет ничего, чтобы создать экземпляр квантификатора. Вы можете проверить его, добавив дополнительные утверждения, чтобы Dafny получал идею использовать эти значения для создания экземпляров квантификаторов.

Например это:

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

Или это

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

Почему это работает

Обычно, когда Dafny нужно что-то доказать с участием квантор он должен выбрать значения для создания экземпляра квант (из-за уменьшения до SAT). Одна из вещей, которые он обычно пытается попробовать, это новая произвольная константа, но это не приведет вас сюда далеко. Вам нужно это, чтобы выбрать значения 0 и 3 (например). Тем не менее, есть много ints, поэтому шансы на выбор таких ценностей наугад низкие - настолько низкие, что на самом деле он даже не попытается. Вместо этого он просматривает любые факты, которые он уже знает, и выбирает любые, которые соответствуют форме атомов в количественной формуле. В этом случае он ищет такие вещи, как a[i]==a[j] - поэтому, вставив в себя утверждение, включающее b[0] и b[3], которое побуждает Dafny в конечном счете попробовать значения 0 и 3 для i и j. Прямая версия b[0]==b[3] работает довольно прямо, а косвенная версия b[0]==t && b[3]==t косвенно вызвать Dafny положить края между b[0] и b[3] в egraph и вывести тот факт, b[0]==b[3] который будет подсказывать, чтобы попытаться 0 и 3 для конкретизации quantifer.

Мне было бы интересно услышать о любых других решениях.

EDIT

Я думал о другом решении using the fuel annotation, но я не знаю, если это действительно лучше решение:

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

predicate noDuplicates (a:seq<char>) 
{ 
    a == [] || (!contains(a[1..], a[0]) && noDuplicates(a[1..])) 
} 

predicate contains (a:seq<char>, v:char) 
{ 
    a != [] && (a[0] == v || contains(a[1..],v)) 
}