Квантификатор Дафни не создается полезно при столкновении с тестовыми данными

Я пытаюсь создать предикат в dafny, который определяет, содержит ли массив символов дубликаты. В конечном итоге он должен проверять что-то вроде: для любых двух элементов в массиве, если значения theor равны, их индекс также должен быть равен. Пожалуйста, игнорируйте случай, когда элементов меньше 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;

dafny
person rohaldb    schedule 10.05.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Я думаю, что проблема в том, что в графе решателя для 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 (например). Однако существует много целых чисел, поэтому шансы выбрать такие значения наугад невелики — настолько малы, что на самом деле он даже не будет пытаться. Вместо этого он просматривает все факты, которые ему уже известны, и выбирает те, которые соответствуют форме атомов в количественной формуле. В этом случае он ищет такие вещи, как a[i]==a[j], поэтому, помещая утверждение, включающее b[0] и b[3], это побуждает Дафни в конечном итоге попробовать значения 0 и 3 для i и j. Прямая версия b[0]==b[3] работает совершенно напрямую, а непрямая версия b[0]==t && b[3]==t косвенно заставит Дафни поместить ребра между b[0] и b[3] в своем эпграфе и вывести факт b[0]==b[3], который затем предложит ей попробовать 0 и 3 для создания экземпляра квантифера.

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

ИЗМЕНИТЬ

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

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)) 
}
person lexicalscope    schedule 10.05.2016
comment
Ваше первое решение сработало отлично. Не могли бы вы объяснить, почему это так? - person rohaldb; 11.05.2016
comment
Обновлено. Суть в том, что вам нужно дать dafny подсказку о том, какие целые числа попробовать для i и j, поскольку возможных целых чисел очень много. - person lexicalscope; 11.05.2016