(*
 * This example shows three operational ways to populate the integer value
 * universe: (1) with a list-constructor; (2) with a recursive operation; (3)
 * with a bounded quantification.
 *
 * Even though values are transient in terms of their local lifetime within
 * populating operations, the values will remain in the value universe after
 * the operation exits.
 *
 * From a practical standpoint, the use of bounded quantification is not all
 * that interesting as the only means to create values to be used subsequently
 * in an unbounded quantification.  I.e., the bounded quantification could be
 * used directly, instead of the unbounded form.  But, unbounded quantification
 * could be OK as a way to generate an initial set of seed values in a
 * universe, with other values generated as additional test execution takes
 * place.
 *)

op PopluateIntUniverseList(lower:integer, upper:integer) = [lower .. upper];

op PopluateIntUniverseRecursive(lower:integer, upper:integer) =
    if lower > upper then nil
    else PopluateIntUniverseRecursive(lower+1, upper);

op PopluateIntUniverseBounded(lower:integer, upper:integer) =
    forall (i in [lower .. upper]) true;

> PopluateIntUniverseList(-100, 100);
> PopluateIntUniverseRecursive(-100, 100);
> PopluateIntUniverseBounded(-100, 100);