Why does Alloy tell me that 3 >= 10?

Question

When debugging a perplexing problem in Alloy, I've used the evaluator to do 3 > 10 and get the result true. Am I missing something?!

Answer 1

Alloy integers are typically very narrow by normal standards, and they normally have a sort of 'wraparound' semantics. In the default scope, in Alloy 4.2 Int ranges from -8 to 7, and literal 8, 9, 10 are indistinguishable from literal -8, -7, -6. (The use of out-of-range values like literal 10 cannot be detected statically, because in principle Alloy models can be infinite; the size of Int is not known statically. It is known dynamically, so it ought to be possible for literals outside the range of Int to raise a dynamic error; I do not know why they don't. It would certainly make life less confusing for some users if they did.)

If you want a constraint like #x > 10, you'll want to specify a larger scope for Int. N.B. the scope given for Int or int specifies the bitwidth used for the twos-complement representation of integers, not the number of Int atoms in the universe.

There is a Forbid Overflow option, which may help (but see this question, which suggests possible complications).

When contemplating using integers in Alloy, it's worthwhile to think about what Jackson says in Software abstractions (discussion following sec. 2.3.2):

Can you really work without interpreted atoms such as the integers?

Yes, almost all the time. And it turns out that on most occasions that you might think you need integers, it's cleaner and more abstract to use atoms of an uninterpreted type with some relations to give whatever interpretation is needed. Alloy does actually support integers, albeit in a restricted way (due to the limitations of finite bounds).

And (discussion after 4.8):

Why leave integers to the end?

Integers are actually not very useful. If you think you need them, think again; there is often a more abstract description that matches the problem better. Just because integers appear in the problem domain does not mean that they should be modeled as such. To figure out whether integers are necessary, ask yourself what properties are actually relied upon. For example, a communications protocol that numbers its messages may rely only on the numbers being distinct; or it may relay on them increasing; or perhaps even being totally ordered. In none of these cases should integers be used. Of course, if you have a heavily numerical problem, you're likely to need integers (and more), but then Alloy is probably not suitable anyway.

Good luck.