Дафни элементы массива, содержащиеся в другом утверждении массива

Question

Дафни элементы массива, содержащиеся в другом утверждении массива

Вопрос довольно прост: почему приведенное ниже утверждение возвращает "нарушение утверждения".

method test()
{
  var a := new int[5];
  a[0] := 1;
  a[1] := 1;
  a[2] := 2;
  a[3] := 3;
  a[4] := 3;
  var b := new int[3];
  b[0] := 1;
  b[1] := 2;
  b[2] := 3;
  assert(forall i :: exists j :: ((0 <= i < 5) && (0 <= j < 3)) ==> (a[i] == b[j]));
}

1

dafny

Источник

user2009400 08 апр '18 в 23:14

1 ответ

Решение

Другие вопросы по тегам dafny

user438267 09 апр '18 в 01:56 2018-04-09 01:56 · Accepted Answer · 2018-04-09 01:56

Вот один из способов исправить это. Добавьте следующие утверждения перед вашим утверждением.

assert b[0] == 1;
assert b[1] == 2;

Кажется, что под квантификатором можно вспомнить только значение самого последнего присвоения bчто объясняет, почему нет дополнительного утверждения о b[2] необходимо.