排列前后的 Dafny 数组成员资格

Question

对数组进行排序后，Dafny 无法验证旧数组中的项目是否存在于已排序的数组中。排序后的数组是旧数组的排列。这里缺少什么？

var a := new int[][100,2,3,4,5];
assert 4 == a[3];
assert 4 in a[..];
sort(a); // in-place array sort, ensures multiset(a[..]) == multiset(old(a[..]))
assert 4 in a[..]; //does not verify. Why?

Dafny 知道新数组已排序。但旧数组中的每个项目并不都存在于新数组中。

Answer 1

问题归结为触发器，您可以将其视为达夫尼用来识别其他事实是真实的事实。该方法释放了多重集前后相等的事实。因此，您的断言必须通过这些触发器来获得您想要的信息。

var a := new int[][100,2,3,4,5];
assert 4 == a[3];
//assert 4 in a[..]; //optional now
assert 4 in multiset(a[..]); //trigger
sort(a);
assert 4 in a[..];