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

Question

如何在合金中建模模算子？

我想尝试合金来证明任何 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

这不编译

Answer 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