Multiset 仅使用一个元素数组进行验证

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} 这两个看起来都很好，但是 Dafny 在 assert ms[2] == 1;。似乎当数组长度 > 1 时会发生这种情况。

我是不是误解了多重集的工作原理，还是有其他问题？

Answer 1

解决方案 1

第二个程序验证您是否在设置 a[0] 和 a[1] 后的某个时间添加 assert a[..] == [2, 3];。例如以下作品：

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;
}

我又不确定为什么这个断言有帮助。

Multiset 仅使用一个元素数组进行验证

Multiset only verifying with one element array

verification

multiset

dafny

解决方案 1

解决方案 2