I looked at the Int implementation in Alloy (i.e., integer.als file in the util directory ) and I come up with the following expressions (aside many others) which I could not understand:
fun add [n1, n2: Int] : Int { this/plus[n1, n2] }
fun plus [n1, n2: Int] : Int { n1 fun/add n2 }
I have two questions:
1) What do the body of these functions mean? ( it seems one calls another! Can anybody please explain how come this implement add!?)
2) Is there any axiomatic definition for the finite Integers (i.e., Int) in Alloy?
I was looking to see if there is any set of axioms which defines Int as a finite subset of natural numbers, i.e., 0 =< Int <= Max. Is there such a thing in Alloy, or it is just using common integers under the hood of these seemingly fake functions .( By the latter statement, I assume the function bodies are fake and this might partly answer my first question!)
this/plus just "calls" the plus function defined in the same file (integer.als); fun/add, on the other hand, calls the built-in add function, which is part of the Alloy implementation, and cannot be defined as a library. The built-in add function implements binary addition of two integers represented in a two's complement, which cannot be done at the Alloy language level.
there is no axiomatic definition of integers in Alloy. Alloy explicitly enumerates all integers within a bitwidth and adds them to the Alloy universe (along with all other atoms)