Promela Reference -- datatypes(2)

Google

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
bit or bool
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)