CODEWITHSUNDEEP
alloy
qartal
qartal

Reputation: 2064

How Int is specified in Alloy

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

Upvotes: 2

Views: 1709

Answers (2)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3857

  1. 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.

  2. 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)

Upvotes: 6

Bernardo Ferreira Bastos Braga
Bernardo Ferreira Bastos Braga

Reputation: 1685

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

Upvotes: 1

Related Questions