Dafny中set集合操作咨询：元素获取、元组访问及元素添加方法

• Dafny 中的set是无序集合类型，本身不存在「第一个元素」的定义，所有元素存储顺序不固定，也不支持按下标直接访问。针对你的第一个疑问，分两种使用场景给出方案：

  • 如果你只需要取出集合中任意一个元组存入变量，可使用choose操作符实现：
    var t := choose x | x in myset;
    取出的元组访问方式和数组中的元组完全一致，用t.0获取元组第一个int值，t.1获取第二个int值即可。
  • 如果你确实需要按固定顺序取出指定位置的元素，可先将set转换为有序序列：
    var myseq := myset.Sequence(); var firstElem := myseq[0];
    转换后得到的myseq是seq<(int,int)>类型，支持按下标访问，取到的元组字段访问规则同上。

• Dafny的set是不可变类型，创建后无法直接修改原有集合的内容，添加元素需要生成新的集合。针对你的第二个疑问，可使用集合的并集操作符+实现：
  示例代码如下：
  myset := myset + {(4, 30)};
  执行后myset就会包含新加入的元组(4,30)。如果需要保留原有集合，也可以赋值给新的变量：
  var new_myset := myset + {(4, 30)};

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