How Int is specified in Alloy

Question

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!)

Aleksandar Milicevic · Accepted Answer · 2015-04-11 16:51:48Z

6

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)

answered Apr 11, 2015 at 16:51

Aleksandar Milicevic

3,8671 gold badge15 silver badges17 bronze badges

Sign up to request clarification or add additional context in comments.

Comments

Bernardo Ferreira Bastos Braga · Accepted Answer · 2015-04-10 14:24:19Z

1

To find the max int, you should search for bitwidth. When you specify the Int scope in a run statement, you specify the bitwidth. For example, if you specify

run{} for 3 Int

You will get integers as big as 3 and as small as -4. The general rule is (2^x-1)-1 for positive numbers and (2^x-1) for negative numbers where X is the scope for Int.

I guess the libs in util/integer are helpers to deal with the tricky Int semantics in Alloy

answered Apr 10, 2015 at 14:24

Bernardo Ferreira Bastos Braga

1,69316 silver badges34 bronze badges

Collectives™ on Stack Overflow

How Int is specified in Alloy

2 Answers 2

Comments

Comments

Your Answer

Linked

Hot Network Questions

Collectives™ on Stack Overflow

2 Answers 2

Comments

Comments

Your Answer

Sign up or log in

Post as a guest

Linked

Related