Initial values of discrete variables

Discrete variables can be given an initial value with their declaration:

disc int x = 1;

The initial value may be omitted, leading to the default value of its data type being used:

disc int x;
disc bool y;

The default value of integer typed variables is 0. The default value of boolean typed variables is false.

It is possible to indicate that a variable has more than one potential initial value:

disc int x in {1, 2, 4};

This declares a variable x that has three potential initial values. Variables can only have one value at a time, so an initial value has to be chosen from the set of potential initial values. In other words, initially the value of variable x is either 1, 2, or 4. For information on how to store multiple values in a single variable, see the lessons on types and values, in particular those on tuples, lists, and sets.

It is also possible to indicate that a variable can have any arbitrary initial value:

disc int x in any;
disc bool y in any;

Variable x can initially have any value. The only constraint is that the initial value must be an integer value, as it must conform to the integer type (int) of the variable. Examples of initial values include -1027, 0, 1, and 12345. Variable y can initially have any value, as long as that value is a boolean value, due to the variable having a boolean type (bool). There are only two boolean values, true and false.

Discrete variables with multiple potential initial values and arbitrary initial values essentially parametrize the specification. The exact initial value is to be chosen or configured later on. This allows a single specification to be used for various different combinations of initial values.

So far all examples used literal values to initialize the variables. However, it is also allowed to use expressions to compute initial values, for instance based on the initial values of other variables:

disc int x = 1;     // Initial value: 1
disc int y = x * 2; // Initial value: 2
disc int z = x + y; // Initial value: 3

Variable x is explicitly initialized with value 1. Variable y is initialized to the initial value of x, multiplied by two. Variable z is initialized to the sum of the initial values of x and y. Using this kind of initialization is useful if the initial values must be kept consistent. Changing the initial value of x automatically also changes the initial values of y and z.

The order of the declaration of the variables does not matter. We could just as easily declare them as follows:

disc int y = x * 2; // Uses variable x, which is declared later.
disc int x = 1;

Variable y is still initialized using the initial value of variable x, which is now declared after variable y. It is not allowed to construct loops, where the initial values of variables depend on each other:

disc int x = y; // Invalid initial value due to cyclic dependency.
disc int y = z;
disc int z = x;

Variable x uses the value of variable y, which uses the value of variable z, which in turn uses the value of variable x again. This is not allowed in CIF, as it creates a cyclic dependency. However, since no restrictions are introduced on the initial values of variables x, y, and z, except that they must be equal to each other, we can declare them as follows:

disc int x in any; // Explicit 'any' breaks the cyclic dependency.
disc int y = z;
disc int z = x;

Here, variable x is explicitly initialized to an arbitrary value. The other variables are initialized to be equal to whatever arbitrary value is chosen as initial value for variable x.