集合排序的定义解析及Alloy中ordering模块的调用疑问

你是不是也困惑过——对无序集合进行排序到底意味着什么？明明集合的定义就是「无序」的，但当我们给集合引入Alloy的ordering模块后，它居然突然拥有了first、last、next、prev这些看起来只有有序结构才有的函数？

拿一个颜色集合来说，比如{red, blue, green}，对它排序到底指什么？调用ordering模块后：

• first会返回什么？
• last又是什么？
• first.next能得到什么？

为了搞清楚这些问题，我们可以用Alloy生成实例来直观理解。比如生成的部分实例可能会出现这些情况：

• 某次实例中，排序后的临时顺序是red → green → blue，那first就是red，last是blue，first.next就是green
• 另一次实例可能生成的顺序是blue → red → green，这时候first变成blue，last是green，first.next是red

这里的核心逻辑其实是：Alloy的ordering模块并没有改变集合本身的「无序」属性，而是给集合中的元素临时赋予了一个随机生成的全序关系（如果没有额外指定排序规则的话）。集合本质上还是无序的，但我们通过ordering给元素加了一个"虚拟"的顺序，这样就能用first、last这些函数来遍历这个临时的有序序列了。

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