合金：事实等等关于诠释

Question

我最近与合金工作。 我可以这样说：

fact{ 
all i: Int | i >= 0 
} 

我想说：所有整数合金的用途应该是积极的。 合金不失败，但也不给我实例。

问候

Answer 1

你目前不能说这个。你可以指定整数的唯一范围（告诉Alloy整数是“使用”）是位宽（例如4 Int）;合金总是使用该位宽内的所有整数（例如，对于4的位宽，使用的整数是-8, ..., 7）。

如果你在你的模型int类型的字段，可以使用一个事实（像你上面说的）来限制它的值：

sig S { i: Int } 
fact { all s: S | s.i >= 0 }