Предикат Дафни ни истинен, ни ложен

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

Этот:

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

dafny
person Calder    schedule 06.07.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Дафни не говорит, что утверждения ложны, он говорит, что не может доказать их истинность. Если вы дадите ему немного больше помощи, то он докажет, что это правда:

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);
}
person lexicalscope    schedule 08.08.2016
comment
Спасибо! Это кажется странным намеком, который нужно дать. :-) - person Calder; 09.08.2016
comment
Это связано с тем, как куча кодируется в Dafny. По сути, Дафни обычно автоматически развертывает индуктивные определения только один раз. Таким образом, он обычно выбирает только последний назначенный элемент массива для создания экземпляров квантификаторов (т. е. единственный элемент, который был назначен в куче current), если вы не сделаете что-то (например, утверждение, которое я написал), что приводит к тому, что другие соответствующие элементы находятся в электронном графе решателей для текущей кучи. По моему опыту, на самом деле лучше работать с формулами (массивами в целом), чем с конкретными значениями (конкретным массивом). - person lexicalscope; 09.08.2016
comment
Есть ли способ определить разницу между я могу доказать, что это неправильно, и я не могу доказать, что это правильно? - person Theodore Norvell; 12.08.2016