如何在Alloy中像声明Int那样声明自然数？

架构老林

2026-7-12

在Alloy中用util/naturals生成简洁自然数集合的可行方案

直接用3 Natural生成的集合会带natural/Natural$前缀，这是因为Natural是util/naturals库定义的自定义签名，并非Alloy内置的原子类型（比如Int）。但可以通过两种方式得到{0,1,2,...}形式的自然数集合：

方法一：直接用Int筛选非负整数
跳过Natural签名，直接基于内置Int类型生成自然数范围，代码示例：
```
fun NatRange(n: Int): set Int {
  { i: Int | i >= 0 and i <= n }
}

run { NatRange(3) } for 4 Int
```
运行后会得到集合{0,1,2,3}，和run 6 Int的输出格式一致。
方法二：提取Natural签名的关联数值
util/naturals库中的Natural签名默认绑定了一个value字段（对应自然数的整数数值），可以通过提取这个字段得到简洁集合：
```
open util/naturals as nat

fun SimpleNats(n: Int): set Int {
  { nv: nat/Natural | nv.value <= n }.value
}

run { SimpleNats(3) } for 4 Int, 4 nat/Natural
```
运行后同样会输出{0,1,2,3}，本质是把带前缀的Natural实例转换成对应的整数数值。