Dafny中如何从集合初始化数组？（已知序列初始化方法）

Dafny里集合是无序结构，而数组依赖有序的索引映射元素，所以要从集合初始化数组，核心是先把集合转换为序列，再沿用你熟悉的序列初始化数组的逻辑实现。

具体实现方式 #

有两种常用写法：

1. 先显式转换集合为序列，再初始化数组

// uniques 是 int 类型的集合
var uniquesSeq := seq(uniques);
var b := new int[|uniquesSeq|](i requires 0 <= i < |uniquesSeq| => uniquesSeq[i]);

2. 直接在数组初始化表达式内完成集合转序列的操作

// uniques 是 int 类型的集合
var b := new int[|uniques|](i requires 0 <= i < |uniques| => seq(uniques)[i]);

额外说明 #

由于集合本身无序，每次转序列的元素顺序可能不确定。如果需要固定顺序，可以先对转换后的序列排序，示例如下：

var sortedSeq := Sort(seq(uniques));
var b := new int[|sortedSeq|](i requires 0 <= i < |sortedSeq| => sortedSeq[i]);

内容的提问来源于stack exchange，提问作者cvl