如何显示合金中的成对序列？

Question

我想知道，如何在合金中定义一对和一对序列？例如，在Z表示法中，我们可以将变量定义（例如c）作为成对的序列，即“ c：seq（A \ cross B）”。合金语言中是否有与此定义等效的东西？

Answer 1

合金非常有表现力，通常您可以将Z直接转换成Alloy。例如，在这种情况下，您可以声明代表对的签名

sig Pair {first, second: X}

然后将字段定义为成对的序列

s: seq Pair

但是通常有更好的方法。例如，也许有两个序列更好。也许这些序列可以表示为顺序；也许您根本不需要序列，集合就可以了。通常，这是人们在使用Alloy进行建模时发现的东西：使事情变得更易于分析也使事情也易于理解和表达。祝你好运！