naturals

Emulates natural (non-negative) numbers.

This is an utility with functions and predicates for using the set of nonnegative integers (0, 1, 2, . . .). The number of naturals present in an analysis will be equal to the scope on Natural. Specifically, if the scope on Natural is N, then the naturals 0 through N-1 will be present.

open util/natural

fun sum[a: Natural, b: Natural]: Natural {
  {x:Natural | x = natural/add[a,b]}
}

run show for 3

To try this module out, in Alloy Analyzer’s evaluator, you may invoke the function defined above as follows:

sum [natural/Natural1, natural/Natural1]
  {natural/Natural$2}

sum [natural/Natural1, natural/Natural2]
  {}

Functions

fun inc [n: Natural]
Return type

one Natural

Returns n + 1.

fun dec [n: Natural]
Return type

one Natural

Returns n - 1.

fun add [n1, n2: Natural]
Return type

one Natural

Returns n1 + n2.

fun sub [n1, n2: Natural]
Return type

one Natural

Returns n1 - n2.

fun mul [n1, n2: Natural]
Return type

one Natural

Returns n1 * n2.

fun div [n1, n2: Natural]
Return type

one Natural

Returns n1 / n2.

fun max [ns: set Natural]
Return type

one Natural

Returns the maximum integer in ns.

fun min [ns: set Natural]
Return type

one Natural

Returns the minimum integer in ns.

Predicates

pred gt [n1, n2: Natural]

True iff n1 is greater than n2.

pred gte [n1, n2: Natural]

True iff n1 is greater than or equal to n2.

pred lt [n1, n2: Natural]

True iff n1 is less than n2.

pred lte [n1, n2: Natural]

True iff n1 is less than or equal to n2.