Многосетевая проверка только с одним массивом элементов

Question

У меня проблема с проверкой, является ли количество элементов в мультимножестве определенным числом. Ниже приведены две программы: одна работает (проверяется правильно), а другая нет.

Проверяет правильно:

method Main() {
  var a: array<int> := new int[1];
  a[0] := 2;
  assert a[0] == 2;

  var ms: multiset<int> := multiset(a[..]);
  print ms;
  assert ms[2] == 1;
}

Не проверяет правильно:

method Main() {
  var a: array<int> := new int[2];
  a[0] := 2;
  a[1] := 3;
  assert a[0] == 2;
  assert a[1] == 3;

  var ms: multiset<int> := multiset(a[..]);
  print ms;
  assert ms[2] == 1;
}

Хотя,прямое использование последовательности, кажется, работает просто отлично:

method Main() {
  var s := [2, 3];
  var ms: multiset<int> := multiset(s);
  print ms;
  assert ms[2] == 1;
}

Я не уверен, почему это происходит. Для первой программы print ms; выводит multiset{2}, а во второй программе print ms; выводит multiset{2, 3}, что, похоже, нормально, но Дафни выдвигает нарушение утверждения для второй в assert ms[2] == 1;. Похоже, это происходит, когда длина массивов> 1.

Я неправильно понимаю, как работают мультимножества, или что-то не так?

Answer 1

Решение 1

Вторая программа проверяет, добавляете ли вы assert a[..] == [2, 3]; через некоторое время после установки a[0] и a[1]. Например, работает следующее:

method Main() {
  var a: array<int> := new int[2];
  a[0] := 2;
  a[1] := 3;
  assert a[0] == 2;
  assert a[1] == 3;

  var ms: multiset<int> := multiset(a[..]);
  assert a[..] == [2, 3];
  print ms;
  assert ms[2] == 1;
}

Я не знаю, почему это утверждение необходимо.

Решение 2

Есть другое решение, которое не требует утвержденияконкретное значение a[..]. Можно определить функцию to_seq(a, i), которая явно вычисляет значение a[i..], а затем assert a[..] == to_seq(a, 0). Более подробно:

function to_seq<T>(a: array<T>, i: int) : (res: seq<T>)
requires 0 <= i <= a.Length
ensures res == a[i..]
reads a
decreases a.Length-i
{
  if i == a.Length
  then []
  else [a[i]] + to_seq(a, i + 1)
}

method Main() {
  var a: array<int> := new int[2];
  a[0] := 2;
  a[1] := 3;

  var ms: multiset<int> := multiset(a[..]);
  assert a[..] == to_seq(a, 0);
  assert ms[2] == 1;
}

Я опять не совсем уверен, почему это утверждение помогает.