如何在合金中建模模运算符？

【问题标题】：How do I model the modulo operator in alloy?如何在合金中建模模运算符？
【发布时间】：2013-09-25 18:48:43
【问题描述】：

如何对合金中的模算子建模？

我想用合金来证明任何 4 的倍数都可以被 2 整除....

这是我的代码..

    //proof that 4n is divisible by 2

    module I4nDivisibleby2

    sig num {}

    fact {
        all n:num|n%4=0
    }

    assert even {
    all n : num | n%2 = 0
    }

    check even for 1

这不会编译

【问题讨论】：

标签： alloy

【解决方案1】：

您应该使用库定义的rem 函数。 rem 函数需要两个整数，因此不能为 num 的实例调用它；相反，你可以做类似的事情

module I4nDivisibleby2

sig num { 
  val: Int
}

fact {
    all n:num | rem[n.val, 4] = 0
}

assert even {
    all n : num | rem[n.val, 2] = 0
}

check even // => no counterexample found

【讨论】：