Promela |
Declarator |
datatypes(2) |
NAME
bit, bool, short, int, unsiged
-
syntax for declaring and initializing variables
of predefined integer data types.
SYNTAX
typename name [ =
anyexpr ] [ ,
name [ =
anyexpr ]
]*
unsigned name : constant
DESCRIPTION
There are six predefined integer data types:
bit ,
bool ,
byte ,
short ,
int ,
and
unsigned .
(There are also constructors for
user-defined data types, see
mtype(2), and
typedef(2), and a predefined data type for message
passing channels, see
chan(2).)
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.
Typename byte short int |
C-equivalent bit-field uchar short int |
Macro in limits.h - CHAR_BIT (width in bits) SHRT_MIN..SHRT_MAX INT_MIN..INT_MAX |
Typical Range 0..1 0..255 -2^15 - 1 .. 2^15 - 1 -2^31 - 1 .. 2^31 - 1 |
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
For instance,
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 scope of a variable declaration is global
if it appears outside all
proctype
(or
init )
declarations. The scope is the complete body of
a process if the declaration appears (anywhere) inside a
proctype
(or
init )
declaration.
Each process has private copies of all variables that are
declared locally in the
proctype
or
init
declaration from which the process is instantiated.
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
arrays(2), chan(2), mtype(2), typedef(2), _(5), _pid(5), run(5).
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |