How do I model the modulo operator in alloy?

Question

How to model the modulo operator in alloy?

I want to try alloy to prove that any multiple of 4 is divisible by 2....

Here's my code..

    //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

This does not compile

Answer 1

You should use the library-defined rem function. The rem function takes two ints, so you can't call it for an instance of num; instead you could do something like

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