|
NAME
SYNTAX
unsigned name : constant DESCRIPTION
Variables of the predefined types can be declared in a C-like style, with a typename that is followed by a comma-separated list of one or more identifier names, each optionally followed by an initializer field. Each variable can also optionally be declared as an array, rather than as a scalar (for this see arrays(2)). The integer data types differ only in the domain of values that a variable of the corresponding type can access. The precise domain can be system dependent in the same way that the corresponding data types in the language C can be system dependent. The dependencies are as follows. Variables of type bit , and bool are stored in a single bit of memory, which means that they can hold only binary (Boolean) values (zero or one, or equivalently true or false ). Variables of type byte are stored in a C variable of type unsigned char, which means on most systems that they can at least hold any positive value in the interval 0..255. Variables of type short are stored in a C variable of type short, which means on most systems that they can at least hold values in the interval -2^15 -1..2^15 -1. Variables of type int are stored in a C variable of type int , which means on most systems that they can hold values in the interval -2^31 -1..2^31 -1. Variables of type unsigned are stored in a bit-field of a size that is specified in the constant that is given as part of the declaration. ISO compliant implementations of C define the precise domains of the first five integer data types in the required header file limits.h . The table below summarizes these definitions.
The default initial value of all variables (declared globally or locally) is zero. If a value is assigned that lies outside the domain of the variable type, the true value assigned is obtained by truncation of the value to the domain (i.e., by a type cast operation). EXAMPLES
byte a, b = 2; short c[3] = 3;declares the names a , and b as variables of type byte , and c as an array variable of type short . Variable a has the default initial value (zero). Variable b is initialized to the constant value 2 , and all three elements of array c are initialized to the value 3 . NOTES
The formal parameters of a proctype are indistinguishable from local variables. These formal parameters are initialized to the values specified in a run statement, or they are initialized to zero when the process is instantiated through an active prefix on the the proctype declaration. Each system has a predefined, write-only, global variable _ (underscore) of type int . Each process has a predefined local variable _pid of type byte , that holds the process instantiation number. The first created process has instantiation number zero. An array of bit , bool , or unsigned variables will be stored as an array of byte variables during verifications. Since this can change the behavior of the program (e.g., if the user relies on automatic truncation effects), the parser warns when this occurs. In the language C, the keyword short may be used as a prefix of int ; the use of short as a prefix is not valid in Promela. SEE ALSO
|