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 naturals.inc [n: Natural]

Return type:: one Natural

Returns n + 1.

fun naturals.dec [n: Natural]

Return type:: one Natural

Returns n - 1.

fun naturals.add [n1, n2: Natural]

Return type:: one Natural

Returns n1 + n2.

fun naturals.sub [n1, n2: Natural]

Return type:: one Natural

Returns n1 - n2.

fun naturals.mul [n1, n2: Natural]

Return type:: one Natural

Returns n1 * n2.

fun naturals.div [n1, n2: Natural]

Return type:: one Natural

Returns n1 / n2.

fun naturals.max [ns: set Natural]

Return type:: one Natural

Returns the maximum integer in ns.

fun naturals.min [ns: set Natural]

Return type:: one Natural

Returns the minimum integer in ns.

Predicates

pred naturals.gt [n1, n2: Natural]: True iff n1 is greater than n2.

pred naturals.gte [n1, n2: Natural]: True iff n1 is greater than or equal to n2.

pred naturals.lt [n1, n2: Natural]: True iff n1 is less than n2.

pred naturals.lte [n1, n2: Natural]: True iff n1 is less than or equal to n2.